Theorem imp31 423

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  imp41  431  imp5d  445  impl  461  anassrs  473  an31s  667  3imp  1128  reusv3  5378  otiunsndisj  5505  pwssun  5555  ordelord  6386  tz7.7  6390  dfimafn  6947  funimass4  6949  funimass3  7053  isomin  7344  isopolem  7352  onint  7795  limsssuc  7852  tfindsg  7863  findsg  7900  suppfnss  8191  smores2  8347  tfrlem9  8378  tz7.49  8438  oecl  8528  oaordi  8537  oaass  8552  omordi  8557  odi  8570  oen0  8578  nnaordi  8610  nnmordi  8623  domunfican  9288  dfac5  10128  cofsmo  10268  cfcoflem  10271  zorn2lem7  10501  tskwun  10786  mulcanpi  10902  ltexprlem7  11044  sup3  12189  elnnz  12618  nzadd  12659  irradd  13015  irrmul  13016  uzsubsubfz  13593  fzo1fzo0n0  13763  elincfzoext  13771  elfzonelfzo  13817  uzindi  14038  ssnn0fi  14041  sqlecan  14265  swrdnd2  14717  swrdwrdsymb  14724  wrd2ind  14784  repswccat  14849  cshwlen  14862  cshwidxmod  14866  2cshwcshw  14888  wrdl3s3  15025  lcmfunsnlem1  16719  coprmprod  16743  unbenlem  16992  infpnlem1  16994  prmgaplem7  17141  iscatd  17753  dirtr  18682  telgsums  20109  zrtermorngc  20794  zrtermoringc  20826  prmidlc  21525  psgndiflemA  21803  isphld  21856  gsummoncoe1  22520  gsummatr01lem3  22866  cpmatmcllem  22927  mp2pm2mplem4  23018  chfacfisf  23063  chfacfisfcpmat  23064  cayleyhamilton1  23101  tgcl  23178  neindisj2  23332  2ndcdisj  23666  fgcl  24088  rnelfm  24163  alexsubALTlem3  24259  2sqreultlem  27664  2sqreunnltlem  27667  elnnzs  28647  usgrexmpledg  29672  cusgrsize  29864  uspgr2wlkeqi  30057  usgr2wlkneq  30171  usgr2pthlem  30178  crctcshwlkn0  30239  wwlksnextinj  30317  wwlksnextproplem2  30328  wwlksnextproplem3  30329  clwlkclwwlklem2a  30418  clwlkclwwlklem2  30420  clwwlkf1  30469  clwwlknwwlksnb  30475  clwwlkext2edg  30476  clwwlknonex2lem2  30528  frgr3vlem1  30697  3vfriswmgrlem  30701  vdgn1frgrv2  30720  frgrwopreglem5  30745  frgrwopreglem5ALT  30746  mdexchi  32760  atomli  32807  mdsymlem5  32832  sumdmdlem  32843  dfimafnf  33054  bnj517  35340  bnj1118  35439  mclsind  36101  dfon2lem6  36317  btwnconn1lem11  36628  finminlem  36888  isbasisrelowllem1  38060  isbasisrelowllem2  38061  poimirlem27  38357  itg2addnc  38384  rngoueqz  38651  dmncan1  38787  disjlem19  39613  lshpdisj  39821  2at0mat0  40359  llncvrlpln2  40391  lplncvrlvol2  40449  pmaple  40595  lhpexle2lem  40843  cdlemk33N  41743  cdlemk34  41744  sn-sup3d  43326  eldioph2  43553  cantnfresb  44111  gneispacess2  44932  sge0iunmpt  47192  funressnfv  47840  dfaimafn  47962  otiunsndisjX  48076  elfz2z  48112  iccelpart  48242  icceuelpart  48245  fargshiftfva  48252  sprsymrelfo  48306  sbcpr  48330  bgoldbtbndlem4  48633  grimcnv  48713  grimco  48714  clnbgrgrim  48759  uspgrlimlem4  48816  grlicsym  48838  grlictr  48840  pgnbgreunbgrlem3  48943  pgnbgreunbgrlem6  48949  idomcanl  49171  snlindsntor  49310  ldepspr  49312  nn0sumshdiglemB  49459