Theorem imp31 417

Description: An importation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
imp31.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
imp31	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem imp31

Step	Hyp	Ref	Expression
1		imp31.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	imp 406	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
3	2	imp 406	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  imp41  425  imp5d  439  impl  455  anassrs  467  an31s  654  3imp  1111  reusv3  5405  otiunsndisj  5525  pwssun  5575  friOLD  5643  ordelord  6406  tz7.7  6410  dfimafn  6971  funimass4  6973  funimass3  7074  isomin  7357  isopolem  7365  onint  7810  limsssuc  7871  tfindsg  7882  findsg  7919  suppfnss  8214  smores2  8394  tfrlem9  8425  tz7.49  8485  oecl  8575  oaordi  8584  oaass  8599  omordi  8604  odi  8617  oen0  8624  nnaordi  8656  nnmordi  8669  php3OLD  9261  domunfican  9361  dfac5  10169  cofsmo  10309  cfcoflem  10312  zorn2lem7  10542  tskwun  10824  mulcanpi  10940  ltexprlem7  11082  sup3  12225  elnnz  12623  nzadd  12665  irradd  13015  irrmul  13016  uzsubsubfz  13586  fzo1fzo0n0  13754  elincfzoext  13762  elfzonelfzo  13808  uzindi  14023  ssnn0fi  14026  sqlecan  14248  swrdnd2  14693  swrdwrdsymb  14700  wrd2ind  14761  repswccat  14824  cshwlen  14837  cshwidxmod  14841  2cshwcshw  14864  wrdl3s3  15001  lcmfunsnlem1  16674  coprmprod  16698  unbenlem  16946  infpnlem1  16948  prmgaplem7  17095  iscatd  17716  dirtr  18647  telgsums  20011  zrtermorngc  20643  zrtermoringc  20675  psgndiflemA  21619  isphld  21672  gsummoncoe1  22312  gsummatr01lem3  22663  cpmatmcllem  22724  mp2pm2mplem4  22815  chfacfisf  22860  chfacfisfcpmat  22861  cayleyhamilton1  22898  tgcl  22976  neindisj2  23131  2ndcdisj  23464  fgcl  23886  rnelfm  23961  alexsubALTlem3  24057  2sqreultlem  27491  2sqreunnltlem  27494  elnnzs  28387  usgrexmpledg  29279  cusgrsize  29472  uspgr2wlkeqi  29666  usgr2wlkneq  29776  usgr2pthlem  29783  crctcshwlkn0  29841  wwlksnextinj  29919  wwlksnextproplem2  29930  wwlksnextproplem3  29931  clwlkclwwlklem2a  30017  clwlkclwwlklem2  30019  clwwlkf1  30068  clwwlknwwlksnb  30074  clwwlkext2edg  30075  clwwlknonex2lem2  30127  frgr3vlem1  30292  3vfriswmgrlem  30296  vdgn1frgrv2  30315  frgrwopreglem5  30340  frgrwopreglem5ALT  30341  mdexchi  32354  atomli  32401  mdsymlem5  32426  sumdmdlem  32437  dfimafnf  32646  prmidlc  33476  bnj517  34899  bnj1118  34998  mclsind  35575  dfon2lem6  35789  btwnconn1lem11  36098  finminlem  36319  isbasisrelowllem1  37356  isbasisrelowllem2  37357  poimirlem27  37654  itg2addnc  37681  rngoueqz  37947  dmncan1  38083  disjlem19  38802  lshpdisj  38988  2at0mat0  39527  llncvrlpln2  39559  lplncvrlvol2  39617  lhpexle2lem  40011  cdlemk33N  40911  cdlemk34  40912  sn-sup3d  42502  eldioph2  42773  cantnfresb  43337  gneispacess2  44159  sge0iunmpt  46433  funressnfv  47055  dfaimafn  47177  otiunsndisjX  47291  elfz2z  47327  iccelpart  47420  icceuelpart  47423  fargshiftfva  47430  sprsymrelfo  47484  sbcpr  47508  bgoldbtbndlem4  47795  grimcnv  47879  grimco  47880  clnbgrgrim  47902  uspgrlimlem4  47958  grlicsym  47973  grlictr  47975  snlindsntor  48388  ldepspr  48390  nn0sumshdiglemB  48541