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  5350  otiunsndisj  5468  pwssun  5516  ordelord  6339  tz7.7  6343  dfimafn  6896  funimass4  6898  funimass3  6999  isomin  7283  isopolem  7291  onint  7735  limsssuc  7792  tfindsg  7803  findsg  7839  suppfnss  8131  smores2  8286  tfrlem9  8316  tz7.49  8376  oecl  8464  oaordi  8473  oaass  8488  omordi  8493  odi  8506  oen0  8514  nnaordi  8546  nnmordi  8559  domunfican  9222  dfac5  10039  cofsmo  10179  cfcoflem  10182  zorn2lem7  10412  tskwun  10695  mulcanpi  10811  ltexprlem7  10953  sup3  12099  elnnz  12498  nzadd  12539  irradd  12886  irrmul  12887  uzsubsubfz  13462  fzo1fzo0n0  13631  elincfzoext  13639  elfzonelfzo  13685  uzindi  13905  ssnn0fi  13908  sqlecan  14132  swrdnd2  14579  swrdwrdsymb  14586  wrd2ind  14646  repswccat  14709  cshwlen  14722  cshwidxmod  14726  2cshwcshw  14748  wrdl3s3  14885  lcmfunsnlem1  16564  coprmprod  16588  unbenlem  16836  infpnlem1  16838  prmgaplem7  16985  iscatd  17596  dirtr  18525  telgsums  19922  zrtermorngc  20576  zrtermoringc  20608  psgndiflemA  21556  isphld  21609  gsummoncoe1  22252  gsummatr01lem3  22601  cpmatmcllem  22662  mp2pm2mplem4  22753  chfacfisf  22798  chfacfisfcpmat  22799  cayleyhamilton1  22836  tgcl  22913  neindisj2  23067  2ndcdisj  23400  fgcl  23822  rnelfm  23897  alexsubALTlem3  23993  2sqreultlem  27414  2sqreunnltlem  27417  elnnzs  28397  usgrexmpledg  29335  cusgrsize  29528  uspgr2wlkeqi  29721  usgr2wlkneq  29829  usgr2pthlem  29836  crctcshwlkn0  29894  wwlksnextinj  29972  wwlksnextproplem2  29983  wwlksnextproplem3  29984  clwlkclwwlklem2a  30073  clwlkclwwlklem2  30075  clwwlkf1  30124  clwwlknwwlksnb  30130  clwwlkext2edg  30131  clwwlknonex2lem2  30183  frgr3vlem1  30348  3vfriswmgrlem  30352  vdgn1frgrv2  30371  frgrwopreglem5  30396  frgrwopreglem5ALT  30397  mdexchi  32410  atomli  32457  mdsymlem5  32482  sumdmdlem  32493  dfimafnf  32714  prmidlc  33529  bnj517  35041  bnj1118  35140  mclsind  35764  dfon2lem6  35980  btwnconn1lem11  36291  finminlem  36512  isbasisrelowllem1  37560  isbasisrelowllem2  37561  poimirlem27  37848  itg2addnc  37875  rngoueqz  38141  dmncan1  38277  disjlem19  39070  lshpdisj  39257  2at0mat0  39795  llncvrlpln2  39827  lplncvrlvol2  39885  pmaple  40031  lhpexle2lem  40279  cdlemk33N  41179  cdlemk34  41180  sn-sup3d  42757  eldioph2  43014  cantnfresb  43576  gneispacess2  44397  sge0iunmpt  46672  funressnfv  47299  dfaimafn  47421  otiunsndisjX  47535  elfz2z  47571  iccelpart  47689  icceuelpart  47692  fargshiftfva  47699  sprsymrelfo  47753  sbcpr  47777  bgoldbtbndlem4  48064  grimcnv  48144  grimco  48145  clnbgrgrim  48190  uspgrlimlem4  48247  grlicsym  48269  grlictr  48271  pgnbgreunbgrlem3  48374  pgnbgreunbgrlem6  48380  snlindsntor  48727  ldepspr  48729  nn0sumshdiglemB  48876