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

Theorem imp31 446
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 443 . 2 ((𝜑𝜓) → (𝜒𝜃))
32imp 443 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  imp41  616  imp5d  622  impl  647  anassrs  677  an31s  843  3imp  1248  3expa  1256  reusv3  4796  otiunsndisj  4895  pwssun  4933  fri  4989  predpo  5600  ordelord  5647  tz7.7  5651  dfimafn  6139  funimass4  6141  funimass3  6225  isomin  6464  isopolem  6472  onint  6864  limsssuc  6919  tfindsg  6929  findsg  6962  suppfnss  7184  smores2  7315  tfrlem9  7345  tz7.49  7404  oecl  7481  oaordi  7490  oaass  7505  omordi  7510  odi  7523  oen0  7530  nnaordi  7562  nnmordi  7575  php3  8008  domunfican  8095  dfac5  8811  cofsmo  8951  cfcoflem  8954  zorn2lem7  9184  tskwun  9462  mulcanpi  9578  ltexprlem7  9720  sup3  10831  elnnz  11222  nzadd  11260  irradd  11646  irrmul  11647  uzsubsubfz  12191  fzo1fzo0n0  12343  elincfzoext  12350  elfzonelfzo  12393  uzindi  12600  ssnn0fi  12603  sqlecan  12790  wrd2ind  13277  repswccat  13331  cshwlen  13344  cshwidxmod  13348  2cshwcshw  13370  wrdl3s3  13501  lcmfunsnlem1  15136  lcmfdvdsb  15142  coprmprod  15161  unbenlem  15398  infpnlem1  15400  prmgaplem7  15547  iscatd  16105  initoeu1  16432  termoeu1  16439  dirtr  17007  telgsums  18161  psrbaglefi  19141  gsummoncoe1  19443  psgndiflemA  19713  isphld  19765  gsummatr01lem3  20229  cpmatmcllem  20289  mp2pm2mplem4  20380  chfacfisf  20425  chfacfisfcpmat  20426  cayleyhamilton1  20463  tgcl  20531  neindisj2  20684  2ndcdisj  21016  fgcl  21439  rnelfm  21514  alexsubALTlem3  21610  usgraexmpledg  25725  usgrares1  25732  usgrafis  25737  nbgraf1olem5  25767  nbcusgra  25785  cusgrares  25794  cusgrasize  25799  usgrwlknloop  25886  pthdepisspth  25897  usgra2adedgspthlem2  25933  usgra2wlkspth  25942  fargshiftfva  25960  usgrcyclnl2  25962  wwlkextinj  26051  wwlkextproplem2  26063  clwlkisclwwlklem2a  26106  clwlkisclwwlklem1  26108  clwwlkf1  26117  clwlkfclwwlk  26164  el2spthonot  26190  2spontn0vne  26207  eupatrl  26288  frgra3vlem1  26320  3vfriswmgralem  26324  vdgn0frgrav2  26344  vdgn1frgrav2  26346  frgrancvvdeqlemC  26359  frgrancvvdgeq  26363  frgrawopreglem5  26368  frg2woteq  26380  usg2spot2nb  26385  2spotmdisj  26388  extwwlkfablem2  26398  numclwwlkovf2ex  26406  mdexchi  28371  atomli  28418  mdsymlem5  28443  sumdmdlem  28454  dfimafnf  28610  bnj517  30002  bnj1118  30099  mclsind  30514  dfon2lem6  30730  btwnconn1lem11  31167  finminlem  31275  isbasisrelowllem1  32162  isbasisrelowllem2  32163  poimirlem27  32389  itg2addnc  32417  rngoueqz  32692  dmncan1  32828  lshpdisj  33075  2at0mat0  33612  llncvrlpln2  33644  lplncvrlvol2  33702  lhpexle2lem  34096  cdlemk33N  34998  cdlemk34  34999  eldioph2  36126  gneispacess2  37247  sge0iunmpt  39094  funressnfv  39640  dfaimafn  39678  iccelpart  39755  icceuelpart  39758  bgoldbtbndlem4  40008  otiunsndisjX  40111  elfz2z  40158  usgrexmpledg  40467  cusgrsize  40651  uspgr2wlkeqi  40837  usgr2pthlem  40950  crctcsh1wlkn0  41005  wwlksnextinj  41086  wwlksnextproplem2  41097  clwlkclwwlklem2a  41188  clwlkclwwlklem2  41190  clwwlksf1  41205  clwwlksext2edg  41211  frgr3vlem1  41424  3vfriswmgrlem  41428  vdgn1frgrv2  41447  frgrncvvdeqlemC  41459  frgrwopreglem5  41466  2wspmdisj  41482  av-numclwwlkovf2ex  41498  zrtermorngc  41774  zrtermoringc  41843  snlindsntor  42035  ldepspr  42037  nn0sumshdiglemB  42193
  Copyright terms: Public domain W3C validator