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  1110  reusv3  5348  otiunsndisj  5466  pwssun  5514  ordelord  6337  tz7.7  6341  dfimafn  6894  funimass4  6896  funimass3  6997  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  9220  dfac5  10037  cofsmo  10177  cfcoflem  10180  zorn2lem7  10410  tskwun  10693  mulcanpi  10809  ltexprlem7  10951  sup3  12097  elnnz  12496  nzadd  12537  irradd  12884  irrmul  12885  uzsubsubfz  13460  fzo1fzo0n0  13629  elincfzoext  13637  elfzonelfzo  13683  uzindi  13903  ssnn0fi  13906  sqlecan  14130  swrdnd2  14577  swrdwrdsymb  14584  wrd2ind  14644  repswccat  14707  cshwlen  14720  cshwidxmod  14724  2cshwcshw  14746  wrdl3s3  14883  lcmfunsnlem1  16562  coprmprod  16586  unbenlem  16834  infpnlem1  16836  prmgaplem7  16983  iscatd  17594  dirtr  18523  telgsums  19920  zrtermorngc  20574  zrtermoringc  20606  psgndiflemA  21554  isphld  21607  gsummoncoe1  22250  gsummatr01lem3  22599  cpmatmcllem  22660  mp2pm2mplem4  22751  chfacfisf  22796  chfacfisfcpmat  22797  cayleyhamilton1  22834  tgcl  22911  neindisj2  23065  2ndcdisj  23398  fgcl  23820  rnelfm  23895  alexsubALTlem3  23991  2sqreultlem  27412  2sqreunnltlem  27415  elnnzs  28359  usgrexmpledg  29284  cusgrsize  29477  uspgr2wlkeqi  29670  usgr2wlkneq  29778  usgr2pthlem  29785  crctcshwlkn0  29843  wwlksnextinj  29921  wwlksnextproplem2  29932  wwlksnextproplem3  29933  clwlkclwwlklem2a  30022  clwlkclwwlklem2  30024  clwwlkf1  30073  clwwlknwwlksnb  30079  clwwlkext2edg  30080  clwwlknonex2lem2  30132  frgr3vlem1  30297  3vfriswmgrlem  30301  vdgn1frgrv2  30320  frgrwopreglem5  30345  frgrwopreglem5ALT  30346  mdexchi  32359  atomli  32406  mdsymlem5  32431  sumdmdlem  32442  dfimafnf  32663  prmidlc  33478  bnj517  34990  bnj1118  35089  mclsind  35713  dfon2lem6  35929  btwnconn1lem11  36240  finminlem  36461  isbasisrelowllem1  37499  isbasisrelowllem2  37500  poimirlem27  37787  itg2addnc  37814  rngoueqz  38080  dmncan1  38216  disjlem19  38999  lshpdisj  39186  2at0mat0  39724  llncvrlpln2  39756  lplncvrlvol2  39814  pmaple  39960  lhpexle2lem  40208  cdlemk33N  41108  cdlemk34  41109  sn-sup3d  42689  eldioph2  42946  cantnfresb  43508  gneispacess2  44329  sge0iunmpt  46604  funressnfv  47231  dfaimafn  47353  otiunsndisjX  47467  elfz2z  47503  iccelpart  47621  icceuelpart  47624  fargshiftfva  47631  sprsymrelfo  47685  sbcpr  47709  bgoldbtbndlem4  47996  grimcnv  48076  grimco  48077  clnbgrgrim  48122  uspgrlimlem4  48179  grlicsym  48201  grlictr  48203  pgnbgreunbgrlem3  48306  pgnbgreunbgrlem6  48312  snlindsntor  48659  ldepspr  48661  nn0sumshdiglemB  48808