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  655  3imp  1111  reusv3  5343  otiunsndisj  5469  pwssun  5517  ordelord  6340  tz7.7  6344  dfimafn  6897  funimass4  6899  funimass3  7001  isomin  7286  isopolem  7294  onint  7738  limsssuc  7795  tfindsg  7806  findsg  7842  suppfnss  8133  smores2  8288  tfrlem9  8318  tz7.49  8378  oecl  8466  oaordi  8475  oaass  8490  omordi  8495  odi  8508  oen0  8516  nnaordi  8548  nnmordi  8561  domunfican  9226  dfac5  10045  cofsmo  10185  cfcoflem  10188  zorn2lem7  10418  tskwun  10701  mulcanpi  10817  ltexprlem7  10959  sup3  12107  elnnz  12528  nzadd  12569  irradd  12917  irrmul  12918  uzsubsubfz  13494  fzo1fzo0n0  13664  elincfzoext  13672  elfzonelfzo  13718  uzindi  13938  ssnn0fi  13941  sqlecan  14165  swrdnd2  14612  swrdwrdsymb  14619  wrd2ind  14679  repswccat  14742  cshwlen  14755  cshwidxmod  14759  2cshwcshw  14781  wrdl3s3  14918  lcmfunsnlem1  16600  coprmprod  16624  unbenlem  16873  infpnlem1  16875  prmgaplem7  17022  iscatd  17633  dirtr  18562  telgsums  19962  zrtermorngc  20614  zrtermoringc  20646  psgndiflemA  21594  isphld  21647  gsummoncoe1  22286  gsummatr01lem3  22635  cpmatmcllem  22696  mp2pm2mplem4  22787  chfacfisf  22832  chfacfisfcpmat  22833  cayleyhamilton1  22870  tgcl  22947  neindisj2  23101  2ndcdisj  23434  fgcl  23856  rnelfm  23931  alexsubALTlem3  24027  2sqreultlem  27427  2sqreunnltlem  27430  elnnzs  28410  usgrexmpledg  29348  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  32727  prmidlc  33526  bnj517  35046  bnj1118  35145  mclsind  35771  dfon2lem6  35987  btwnconn1lem11  36298  finminlem  36519  isbasisrelowllem1  37688  isbasisrelowllem2  37689  poimirlem27  37985  itg2addnc  38012  rngoueqz  38278  dmncan1  38414  disjlem19  39242  lshpdisj  39450  2at0mat0  39988  llncvrlpln2  40020  lplncvrlvol2  40078  pmaple  40224  lhpexle2lem  40472  cdlemk33N  41372  cdlemk34  41373  sn-sup3d  42954  eldioph2  43211  cantnfresb  43773  gneispacess2  44594  sge0iunmpt  46867  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