MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imp31 Structured version   Visualization version   GIF version

Theorem imp31 448
Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
impd.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
imp31 (((𝜑𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem imp31
StepHypRef Expression
1 impd.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21imp 445 . 2 ((𝜑𝜓) → (𝜒𝜃))
32imp 445 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 386
This theorem is referenced by:  imp41  618  imp5d  624  impl  649  anassrs  679  an31s  847  3imp  1254  3expa  1263  reusv3  4867  otiunsndisj  4970  pwssun  5010  fri  5066  predpo  5686  ordelord  5733  tz7.7  5737  dfimafn  6232  funimass4  6234  funimass3  6319  isomin  6572  isopolem  6580  onint  6980  limsssuc  7035  tfindsg  7045  findsg  7078  suppfnss  7305  smores2  7436  tfrlem9  7466  tz7.49  7525  oecl  7602  oaordi  7611  oaass  7626  omordi  7631  odi  7644  oen0  7651  nnaordi  7683  nnmordi  7696  php3  8131  domunfican  8218  dfac5  8936  cofsmo  9076  cfcoflem  9079  zorn2lem7  9309  tskwun  9591  mulcanpi  9707  ltexprlem7  9849  sup3  10965  elnnz  11372  nzadd  11410  irradd  11797  irrmul  11798  uzsubsubfz  12348  fzo1fzo0n0  12502  elincfzoext  12509  elfzonelfzo  12554  uzindi  12764  ssnn0fi  12767  sqlecan  12954  wrd2ind  13459  repswccat  13513  cshwlen  13526  cshwidxmod  13530  2cshwcshw  13552  wrdl3s3  13686  lcmfunsnlem1  15331  lcmfdvdsb  15337  coprmprod  15356  unbenlem  15593  infpnlem1  15595  prmgaplem7  15742  iscatd  16315  initoeu1  16642  termoeu1  16649  dirtr  17217  telgsums  18371  psrbaglefi  19353  gsummoncoe1  19655  psgndiflemA  19928  isphld  19980  gsummatr01lem3  20444  cpmatmcllem  20504  mp2pm2mplem4  20595  chfacfisf  20640  chfacfisfcpmat  20641  cayleyhamilton1  20678  tgcl  20754  neindisj2  20908  2ndcdisj  21240  fgcl  21663  rnelfm  21738  alexsubALTlem3  21834  usgrexmpledg  26135  cusgrsize  26331  uspgr2wlkeqi  26525  usgr2wlkneq  26633  usgr2pthlem  26640  crctcshwlkn0  26694  wwlksnextinj  26775  wwlksnextproplem2  26786  clwlkclwwlklem2a  26880  clwlkclwwlklem2  26882  clwwlksf1  26897  clwwlksext2edg  26903  frgr3vlem1  27117  3vfriswmgrlem  27121  vdgn1frgrv2  27140  frgrwopreglem5  27158  numclwwlkovf2ex  27191  mdexchi  29164  atomli  29211  mdsymlem5  29236  sumdmdlem  29247  dfimafnf  29409  bnj517  30929  bnj1118  31026  mclsind  31441  dfon2lem6  31667  btwnconn1lem11  32179  finminlem  32287  bj-snmoore  33043  isbasisrelowllem1  33174  isbasisrelowllem2  33175  poimirlem27  33407  itg2addnc  33435  rngoueqz  33710  dmncan1  33846  lshpdisj  34093  2at0mat0  34630  llncvrlpln2  34662  lplncvrlvol2  34720  lhpexle2lem  35114  cdlemk33N  36016  cdlemk34  36017  eldioph2  37144  gneispacess2  38264  sge0iunmpt  40398  funressnfv  40971  dfaimafn  41008  otiunsndisjX  41061  elfz2z  41088  iccelpart  41133  icceuelpart  41136  fargshiftfva  41143  bgoldbtbndlem4  41461  sprsymrelfo  41512  zrtermorngc  41766  zrtermoringc  41835  snlindsntor  42025  ldepspr  42027  nn0sumshdiglemB  42179
  Copyright terms: Public domain W3C validator