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  5363  otiunsndisj  5483  pwssun  5533  ordelord  6357  tz7.7  6361  dfimafn  6926  funimass4  6928  funimass3  7029  isomin  7315  isopolem  7323  onint  7769  limsssuc  7829  tfindsg  7840  findsg  7876  suppfnss  8171  smores2  8326  tfrlem9  8356  tz7.49  8416  oecl  8504  oaordi  8513  oaass  8528  omordi  8533  odi  8546  oen0  8553  nnaordi  8585  nnmordi  8598  domunfican  9279  dfac5  10089  cofsmo  10229  cfcoflem  10232  zorn2lem7  10462  tskwun  10744  mulcanpi  10860  ltexprlem7  11002  sup3  12147  elnnz  12546  nzadd  12588  irradd  12939  irrmul  12940  uzsubsubfz  13514  fzo1fzo0n0  13683  elincfzoext  13691  elfzonelfzo  13737  uzindi  13954  ssnn0fi  13957  sqlecan  14181  swrdnd2  14627  swrdwrdsymb  14634  wrd2ind  14695  repswccat  14758  cshwlen  14771  cshwidxmod  14775  2cshwcshw  14798  wrdl3s3  14935  lcmfunsnlem1  16614  coprmprod  16638  unbenlem  16886  infpnlem1  16888  prmgaplem7  17035  iscatd  17641  dirtr  18568  telgsums  19930  zrtermorngc  20559  zrtermoringc  20591  psgndiflemA  21517  isphld  21570  gsummoncoe1  22202  gsummatr01lem3  22551  cpmatmcllem  22612  mp2pm2mplem4  22703  chfacfisf  22748  chfacfisfcpmat  22749  cayleyhamilton1  22786  tgcl  22863  neindisj2  23017  2ndcdisj  23350  fgcl  23772  rnelfm  23847  alexsubALTlem3  23943  2sqreultlem  27365  2sqreunnltlem  27368  elnnzs  28296  usgrexmpledg  29196  cusgrsize  29389  uspgr2wlkeqi  29583  usgr2wlkneq  29693  usgr2pthlem  29700  crctcshwlkn0  29758  wwlksnextinj  29836  wwlksnextproplem2  29847  wwlksnextproplem3  29848  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  clwwlkf1  29985  clwwlknwwlksnb  29991  clwwlkext2edg  29992  clwwlknonex2lem2  30044  frgr3vlem1  30209  3vfriswmgrlem  30213  vdgn1frgrv2  30232  frgrwopreglem5  30257  frgrwopreglem5ALT  30258  mdexchi  32271  atomli  32318  mdsymlem5  32343  sumdmdlem  32354  dfimafnf  32567  prmidlc  33426  bnj517  34882  bnj1118  34981  mclsind  35564  dfon2lem6  35783  btwnconn1lem11  36092  finminlem  36313  isbasisrelowllem1  37350  isbasisrelowllem2  37351  poimirlem27  37648  itg2addnc  37675  rngoueqz  37941  dmncan1  38077  disjlem19  38800  lshpdisj  38987  2at0mat0  39526  llncvrlpln2  39558  lplncvrlvol2  39616  lhpexle2lem  40010  cdlemk33N  40910  cdlemk34  40911  sn-sup3d  42487  eldioph2  42757  cantnfresb  43320  gneispacess2  44142  sge0iunmpt  46423  funressnfv  47048  dfaimafn  47170  otiunsndisjX  47284  elfz2z  47320  iccelpart  47438  icceuelpart  47441  fargshiftfva  47448  sprsymrelfo  47502  sbcpr  47526  bgoldbtbndlem4  47813  grimcnv  47892  grimco  47893  clnbgrgrim  47938  uspgrlimlem4  47994  grlicsym  48009  grlictr  48011  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118  snlindsntor  48464  ldepspr  48466  nn0sumshdiglemB  48613