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

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

Proof of Theorem imp31
StepHypRef Expression
1 imp31.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21imp 395 . 2 ((𝜑𝜓) → (𝜒𝜃))
32imp 395 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 198  df-an 385
This theorem is referenced by:  imp41  414  imp5d  428  impl  445  anassrs  455  an31s  636  3imp  1130  3impOLD  1131  3expaOLD  1439  reusv3  5074  otiunsndisj  5175  pwssun  5215  fri  5273  predpo  5911  ordelord  5958  tz7.7  5962  dfimafn  6466  funimass4  6468  funimass3  6555  isomin  6811  isopolem  6819  onint  7225  limsssuc  7280  tfindsg  7290  findsg  7323  suppfnss  7554  suppfnssOLD  7555  smores2  7687  tfrlem9  7717  tz7.49  7776  oecl  7854  oaordi  7863  oaass  7878  omordi  7883  odi  7896  oen0  7903  nnaordi  7935  nnmordi  7948  php3  8385  domunfican  8472  dfac5  9234  cofsmo  9376  cfcoflem  9379  zorn2lem7  9609  tskwun  9891  mulcanpi  10007  ltexprlem7  10149  sup3  11265  elnnz  11653  nzadd  11691  irradd  12031  irrmul  12032  uzsubsubfz  12586  fzo1fzo0n0  12743  elincfzoext  12750  elfzonelfzo  12794  uzindi  13005  ssnn0fi  13008  sqlecan  13194  wrd2ind  13701  repswccat  13756  cshwlen  13769  cshwidxmod  13773  2cshwcshw  13795  wrdl3s3  13930  lcmfunsnlem1  15569  lcmfdvdsb  15575  coprmprod  15593  unbenlem  15829  infpnlem1  15831  prmgaplem7  15978  iscatd  16538  initoeu1  16865  termoeu1  16872  dirtr  17441  telgsums  18592  psrbaglefi  19581  gsummoncoe1  19882  psgndiflemA  20155  isphld  20209  gsummatr01lem3  20675  cpmatmcllem  20736  mp2pm2mplem4  20827  chfacfisf  20872  chfacfisfcpmat  20873  cayleyhamilton1  20910  tgcl  20987  neindisj2  21141  2ndcdisj  21473  fgcl  21895  rnelfm  21970  alexsubALTlem3  22066  usgrexmpledg  26370  cusgrsize  26578  uspgr2wlkeqi  26772  usgr2wlkneq  26880  usgr2pthlem  26887  crctcshwlkn0  26942  wwlksnextinj  27036  wwlksnextproplem2  27048  clwlkclwwlklem2a  27141  clwlkclwwlklem2  27143  clwwlkf1  27198  clwwlknwwlksnb  27205  clwwlkext2edg  27206  wwlksext2clwwlk  27207  clwwlknonex2lem2  27277  frgr3vlem1  27448  3vfriswmgrlem  27452  vdgn1frgrv2  27471  frgrwopreglem5  27496  frgrwopreglem5ALT  27497  mdexchi  29522  atomli  29569  mdsymlem5  29594  sumdmdlem  29605  dfimafnf  29763  bnj517  31278  bnj1118  31375  mclsind  31790  dfon2lem6  32013  btwnconn1lem11  32525  finminlem  32633  bj-snmoore  33379  isbasisrelowllem1  33519  isbasisrelowllem2  33520  poimirlem27  33749  itg2addnc  33776  rngoueqz  34050  dmncan1  34186  lshpdisj  34767  2at0mat0  35305  llncvrlpln2  35337  lplncvrlvol2  35395  lhpexle2lem  35789  cdlemk33N  36690  cdlemk34  36691  eldioph2  37827  gneispacess2  38944  sge0iunmpt  41114  funressnfv  41662  dfaimafn  41754  otiunsndisjX  41869  elfz2z  41900  iccelpart  41944  icceuelpart  41947  fargshiftfva  41954  bgoldbtbndlem4  42271  sprsymrelfo  42315  zrtermorngc  42569  zrtermoringc  42638  snlindsntor  42828  ldepspr  42830  nn0sumshdiglemB  42982
  Copyright terms: Public domain W3C validator