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

Theorem imp31 447
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 444 . 2 ((𝜑𝜓) → (𝜒𝜃))
32imp 444 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 385
This theorem is referenced by:  imp41  618  imp5d  624  impl  649  anassrs  681  an31s  865  3imp  1275  3expa  1284  reusv3  4906  otiunsndisj  5009  pwssun  5049  fri  5105  predpo  5736  ordelord  5783  tz7.7  5787  dfimafn  6284  funimass4  6286  funimass3  6373  isomin  6627  isopolem  6635  onint  7037  limsssuc  7092  tfindsg  7102  findsg  7135  suppfnss  7365  smores2  7496  tfrlem9  7526  tz7.49  7585  oecl  7662  oaordi  7671  oaass  7686  omordi  7691  odi  7704  oen0  7711  nnaordi  7743  nnmordi  7756  php3  8187  domunfican  8274  dfac5  8989  cofsmo  9129  cfcoflem  9132  zorn2lem7  9362  tskwun  9644  mulcanpi  9760  ltexprlem7  9902  sup3  11018  elnnz  11425  nzadd  11463  irradd  11850  irrmul  11851  uzsubsubfz  12401  fzo1fzo0n0  12558  elincfzoext  12565  elfzonelfzo  12610  uzindi  12821  ssnn0fi  12824  sqlecan  13011  wrd2ind  13523  repswccat  13578  cshwlen  13591  cshwidxmod  13595  2cshwcshw  13617  wrdl3s3  13751  lcmfunsnlem1  15397  lcmfdvdsb  15403  coprmprod  15422  unbenlem  15659  infpnlem1  15661  prmgaplem7  15808  iscatd  16381  initoeu1  16708  termoeu1  16715  dirtr  17283  telgsums  18436  psrbaglefi  19420  gsummoncoe1  19722  psgndiflemA  19995  isphld  20047  gsummatr01lem3  20511  cpmatmcllem  20571  mp2pm2mplem4  20662  chfacfisf  20707  chfacfisfcpmat  20708  cayleyhamilton1  20745  tgcl  20821  neindisj2  20975  2ndcdisj  21307  fgcl  21729  rnelfm  21804  alexsubALTlem3  21900  usgrexmpledg  26199  cusgrsize  26406  uspgr2wlkeqi  26600  usgr2wlkneq  26708  usgr2pthlem  26715  crctcshwlkn0  26769  wwlksnextinj  26862  wwlksnextproplem2  26873  clwlkclwwlklem2a  26964  clwlkclwwlklem2  26966  clwwlkf1  27012  clwwlknwwlksnb  27019  clwwlkext2edg  27020  wwlksext2clwwlk  27021  clwwlknonex2lem2  27083  frgr3vlem1  27253  3vfriswmgrlem  27257  vdgn1frgrv2  27276  frgrwopreglem5  27301  frgrwopreglem5ALT  27302  mdexchi  29322  atomli  29369  mdsymlem5  29394  sumdmdlem  29405  dfimafnf  29564  bnj517  31081  bnj1118  31178  mclsind  31593  dfon2lem6  31817  btwnconn1lem11  32329  finminlem  32437  bj-snmoore  33193  isbasisrelowllem1  33333  isbasisrelowllem2  33334  poimirlem27  33566  itg2addnc  33594  rngoueqz  33869  dmncan1  34005  lshpdisj  34592  2at0mat0  35129  llncvrlpln2  35161  lplncvrlvol2  35219  lhpexle2lem  35613  cdlemk33N  36514  cdlemk34  36515  eldioph2  37642  gneispacess2  38761  sge0iunmpt  40953  funressnfv  41529  dfaimafn  41566  otiunsndisjX  41621  elfz2z  41650  iccelpart  41694  icceuelpart  41697  fargshiftfva  41704  bgoldbtbndlem4  42021  sprsymrelfo  42072  zrtermorngc  42326  zrtermoringc  42395  snlindsntor  42585  ldepspr  42587  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator