Theorem imp31 418

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 407	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
3	2	imp 407	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  imp41  426  imp5d  440  impl  456  anassrs  468  an31s  652  3imp  1111  reusv3  5403  otiunsndisj  5520  pwssun  5571  friOLD  5637  ordelord  6386  tz7.7  6390  dfimafn  6954  funimass4  6956  funimass3  7055  isomin  7336  isopolem  7344  onint  7780  limsssuc  7841  tfindsg  7852  findsg  7892  suppfnss  8176  smores2  8356  tfrlem9  8387  tz7.49  8447  oecl  8539  oaordi  8548  oaass  8563  omordi  8568  odi  8581  oen0  8588  nnaordi  8620  nnmordi  8633  php3OLD  9226  domunfican  9322  dfac5  10125  cofsmo  10266  cfcoflem  10269  zorn2lem7  10499  tskwun  10781  mulcanpi  10897  ltexprlem7  11039  sup3  12175  elnnz  12572  nzadd  12614  irradd  12961  irrmul  12962  uzsubsubfz  13527  fzo1fzo0n0  13687  elincfzoext  13694  elfzonelfzo  13738  uzindi  13951  ssnn0fi  13954  sqlecan  14177  swrdnd2  14609  swrdwrdsymb  14616  wrd2ind  14677  repswccat  14740  cshwlen  14753  cshwidxmod  14757  2cshwcshw  14780  wrdl3s3  14917  lcmfunsnlem1  16578  coprmprod  16602  unbenlem  16845  infpnlem1  16847  prmgaplem7  16994  iscatd  17621  dirtr  18559  telgsums  19902  psgndiflemA  21373  isphld  21426  psrbaglefiOLD  21705  gsummoncoe1  22048  gsummatr01lem3  22379  cpmatmcllem  22440  mp2pm2mplem4  22531  chfacfisf  22576  chfacfisfcpmat  22577  cayleyhamilton1  22614  tgcl  22692  neindisj2  22847  2ndcdisj  23180  fgcl  23602  rnelfm  23677  alexsubALTlem3  23773  2sqreultlem  27174  2sqreunnltlem  27177  usgrexmpledg  28774  cusgrsize  28966  uspgr2wlkeqi  29160  usgr2wlkneq  29268  usgr2pthlem  29275  crctcshwlkn0  29330  wwlksnextinj  29408  wwlksnextproplem2  29419  wwlksnextproplem3  29420  clwlkclwwlklem2a  29506  clwlkclwwlklem2  29508  clwwlkf1  29557  clwwlknwwlksnb  29563  clwwlkext2edg  29564  clwwlknonex2lem2  29616  frgr3vlem1  29781  3vfriswmgrlem  29785  vdgn1frgrv2  29804  frgrwopreglem5  29829  frgrwopreglem5ALT  29830  mdexchi  31843  atomli  31890  mdsymlem5  31915  sumdmdlem  31926  dfimafnf  32115  prmidlc  32829  bnj517  34182  bnj1118  34281  mclsind  34847  dfon2lem6  35052  btwnconn1lem11  35361  finminlem  35506  isbasisrelowllem1  36539  isbasisrelowllem2  36540  poimirlem27  36818  itg2addnc  36845  rngoueqz  37111  dmncan1  37247  disjlem19  37974  lshpdisj  38160  2at0mat0  38699  llncvrlpln2  38731  lplncvrlvol2  38789  lhpexle2lem  39183  cdlemk33N  40083  cdlemk34  40084  eldioph2  41802  cantnfresb  42376  gneispacess2  43199  sge0iunmpt  45433  funressnfv  46052  dfaimafn  46172  otiunsndisjX  46286  elfz2z  46322  iccelpart  46400  icceuelpart  46403  fargshiftfva  46410  sprsymrelfo  46464  sbcpr  46488  bgoldbtbndlem4  46775  isomuspgrlem1  46794  isomuspgrlem2b  46796  isomuspgrlem2d  46798  zrtermorngc  46988  zrtermoringc  47057  snlindsntor  47240  ldepspr  47242  nn0sumshdiglemB  47394