Theorem imp31 423

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 412	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
3	2	imp 412	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  imp41  431  imp5d  445  impl  461  anassrs  473  an31s  667  3imp  1128  reusv3  5367  otiunsndisj  5493  pwssun  5543  ordelord  6384  tz7.7  6388  dfimafn  6947  funimass4  6949  funimass3  7053  isomin  7345  isopolem  7353  onint  7804  limsssuc  7861  tfindsg  7872  findsg  7909  suppfnss  8206  smores2  8362  tfrlem9  8393  tz7.49  8455  oecl  8545  oaordi  8554  oaass  8569  omordi  8574  odi  8587  oen0  8595  nnaordi  8627  nnmordi  8640  domunfican  9313  dfac5  10207  cofsmo  10347  cfcoflem  10350  zorn2lem7  10580  tskwun  10869  mulcanpi  10985  ltexprlem7  11127  sup3  12274  elnnz  12703  nzadd  12744  irradd  13101  irrmul  13102  uzsubsubfz  13680  fzo1fzo0n0  13850  elincfzoext  13858  elfzonelfzo  13904  uzindi  14125  ssnn0fi  14128  sqlecan  14353  swrdnd2  14805  swrdwrdsymb  14812  wrd2ind  14872  repswccat  14937  cshwlen  14950  cshwidxmod  14954  2cshwcshw  14976  wrdl3s3  15115  lcmfunsnlem1  16812  coprmprod  16836  unbenlem  17086  infpnlem1  17088  prmgaplem7  17235  iscatd  17847  dirtr  18776  telgsums  20207  zrtermorngc  20895  zrtermoringc  20927  prmidlc  21629  psgndiflemA  21907  isphld  21960  gsummoncoe1  22626  gsummatr01lem3  22972  cpmatmcllem  23036  mp2pm2mplem4  23127  chfacfisf  23172  chfacfisfcpmat  23173  cayleyhamilton1  23210  tgcl  23287  neindisj2  23441  2ndcdisj  23775  fgcl  24197  rnelfm  24272  alexsubALTlem3  24368  2sqreultlem  27774  2sqreunnltlem  27777  elnnzs  28787  usgrexmpledg  29843  cusgrsize  30035  uspgr2wlkeqi  30228  usgr2wlkneq  30342  usgr2pthlem  30349  crctcshwlkn0  30410  wwlksnextinj  30488  wwlksnextproplem2  30499  wwlksnextproplem3  30500  clwlkclwwlklem2a  30589  clwlkclwwlklem2  30591  clwwlkf1  30640  clwwlknwwlksnb  30646  clwwlkext2edg  30647  clwwlknonex2lem2  30699  frgr3vlem1  30874  3vfriswmgrlem  30878  vdgn1frgrv2  30897  frgrwopreglem5  30922  frgrwopreglem5ALT  30923  mdexchi  32937  atomli  32984  mdsymlem5  33009  sumdmdlem  33020  dfimafnf  33230  bnj517  35515  bnj1118  35614  mclsind  36335  dfon2lem6  36550  btwnconn1lem11  36862  finminlem  37106  isbasisrelowllem1  38278  isbasisrelowllem2  38279  poimirlem27  38565  itg2addnc  38592  rngoueqz  38874  dmncan1  39010  disjlem19  39836  lshpdisj  40044  2at0mat0  40582  llncvrlpln2  40614  lplncvrlvol2  40672  pmaple  40818  lhpexle2lem  41066  cdlemk33N  41966  cdlemk34  41967  sn-sup3d  43556  eldioph2  43772  cantnfresb  44325  gneispacess2  45145  sge0iunmpt  47427  funressnfv  48112  dfaimafn  48234  otiunsndisjX  48348  elfz2z  48384  iccelpart  48514  icceuelpart  48517  fargshiftfva  48524  sprsymrelfo  48578  sbcpr  48602  bgoldbtbndlem4  48905  grimcnv  48985  grimco  48986  clnbgrgrim  49031  uspgrlimlem4  49088  grlicsym  49110  grlictr  49112  pgnbgreunbgrlem3  49215  pgnbgreunbgrlem6  49221  idomcanl  49443  snlindsntor  49582  ldepspr  49584  nn0sumshdiglemB  49731