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

This theorem is referenced by:  imp41  426  imp5d  440  impl  456  anassrs  468  an31s  660  3imp  1116  reusv3  5334  otiunsndisj  5461  pwssun  5510  ordelord  6332  tz7.7  6336  dfimafn  6889  funimass4  6891  funimass3  6995  isomin  7281  isopolem  7289  onint  7733  limsssuc  7790  tfindsg  7801  findsg  7837  suppfnss  8129  smores2  8284  tfrlem9  8314  tz7.49  8374  oecl  8462  oaordi  8471  oaass  8486  omordi  8491  odi  8504  oen0  8512  nnaordi  8544  nnmordi  8557  domunfican  9222  dfac5  10042  cofsmo  10182  cfcoflem  10185  zorn2lem7  10415  tskwun  10698  mulcanpi  10814  ltexprlem7  10956  sup3  12104  elnnz  12525  nzadd  12566  irradd  12914  irrmul  12915  uzsubsubfz  13491  fzo1fzo0n0  13661  elincfzoext  13669  elfzonelfzo  13715  uzindi  13935  ssnn0fi  13938  sqlecan  14162  swrdnd2  14609  swrdwrdsymb  14616  wrd2ind  14676  repswccat  14739  cshwlen  14752  cshwidxmod  14756  2cshwcshw  14778  wrdl3s3  14915  lcmfunsnlem1  16597  coprmprod  16621  unbenlem  16870  infpnlem1  16872  prmgaplem7  17019  iscatd  17630  dirtr  18559  telgsums  19959  zrtermorngc  20615  zrtermoringc  20647  psgndiflemA  21576  isphld  21629  gsummoncoe1  22294  gsummatr01lem3  22640  cpmatmcllem  22701  mp2pm2mplem4  22792  chfacfisf  22837  chfacfisfcpmat  22838  cayleyhamilton1  22875  tgcl  22952  neindisj2  23106  2ndcdisj  23439  fgcl  23861  rnelfm  23936  alexsubALTlem3  24032  2sqreultlem  27428  2sqreunnltlem  27431  elnnzs  28411  usgrexmpledg  29349  cusgrsize  29541  uspgr2wlkeqi  29734  usgr2wlkneq  29842  usgr2pthlem  29849  crctcshwlkn0  29907  wwlksnextinj  29985  wwlksnextproplem2  29996  wwlksnextproplem3  29997  clwlkclwwlklem2a  30086  clwlkclwwlklem2  30088  clwwlkf1  30137  clwwlknwwlksnb  30143  clwwlkext2edg  30144  clwwlknonex2lem2  30196  frgr3vlem1  30361  3vfriswmgrlem  30365  vdgn1frgrv2  30384  frgrwopreglem5  30409  frgrwopreglem5ALT  30410  mdexchi  32424  atomli  32471  mdsymlem5  32496  sumdmdlem  32507  dfimafnf  32728  prmidlc  33531  bnj517  35067  bnj1118  35166  mclsind  35798  dfon2lem6  36014  btwnconn1lem11  36325  finminlem  36546  isbasisrelowllem1  37717  isbasisrelowllem2  37718  poimirlem27  38014  itg2addnc  38041  rngoueqz  38307  dmncan1  38443  disjlem19  39271  lshpdisj  39479  2at0mat0  40017  llncvrlpln2  40049  lplncvrlvol2  40107  pmaple  40253  lhpexle2lem  40501  cdlemk33N  41401  cdlemk34  41402  sn-sup3d  42982  eldioph2  43211  cantnfresb  43769  gneispacess2  44590  sge0iunmpt  46861  funressnfv  47506  dfaimafn  47628  otiunsndisjX  47742  elfz2z  47778  iccelpart  47908  icceuelpart  47911  fargshiftfva  47918  sprsymrelfo  47972  sbcpr  47996  bgoldbtbndlem4  48299  grimcnv  48379  grimco  48380  clnbgrgrim  48425  uspgrlimlem4  48482  grlicsym  48504  grlictr  48506  pgnbgreunbgrlem3  48609  pgnbgreunbgrlem6  48615  snlindsntor  48962  ldepspr  48964  nn0sumshdiglemB  49111