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  5370  otiunsndisj  5497  pwssun  5547  ordelord  6379  tz7.7  6383  dfimafn  6941  funimass4  6943  funimass3  7047  isomin  7339  isopolem  7347  onint  7790  limsssuc  7847  tfindsg  7858  findsg  7895  suppfnss  8188  smores2  8344  tfrlem9  8375  tz7.49  8437  oecl  8527  oaordi  8536  oaass  8551  omordi  8556  odi  8569  oen0  8577  nnaordi  8609  nnmordi  8622  domunfican  9294  dfac5  10134  cofsmo  10274  cfcoflem  10277  zorn2lem7  10507  tskwun  10796  mulcanpi  10912  ltexprlem7  11054  sup3  12199  elnnz  12628  nzadd  12669  irradd  13026  irrmul  13027  uzsubsubfz  13604  fzo1fzo0n0  13774  elincfzoext  13782  elfzonelfzo  13828  uzindi  14049  ssnn0fi  14052  sqlecan  14276  swrdnd2  14728  swrdwrdsymb  14735  wrd2ind  14795  repswccat  14860  cshwlen  14873  cshwidxmod  14877  2cshwcshw  14899  wrdl3s3  15038  lcmfunsnlem1  16730  coprmprod  16754  unbenlem  17003  infpnlem1  17005  prmgaplem7  17152  iscatd  17764  dirtr  18693  telgsums  20123  zrtermorngc  20808  zrtermoringc  20840  prmidlc  21539  psgndiflemA  21817  isphld  21870  gsummoncoe1  22536  gsummatr01lem3  22882  cpmatmcllem  22946  mp2pm2mplem4  23037  chfacfisf  23082  chfacfisfcpmat  23083  cayleyhamilton1  23120  tgcl  23197  neindisj2  23351  2ndcdisj  23685  fgcl  24107  rnelfm  24182  alexsubALTlem3  24278  2sqreultlem  27686  2sqreunnltlem  27689  elnnzs  28669  usgrexmpledg  29725  cusgrsize  29917  uspgr2wlkeqi  30110  usgr2wlkneq  30224  usgr2pthlem  30231  crctcshwlkn0  30292  wwlksnextinj  30370  wwlksnextproplem2  30381  wwlksnextproplem3  30382  clwlkclwwlklem2a  30471  clwlkclwwlklem2  30473  clwwlkf1  30522  clwwlknwwlksnb  30528  clwwlkext2edg  30529  clwwlknonex2lem2  30581  frgr3vlem1  30756  3vfriswmgrlem  30760  vdgn1frgrv2  30779  frgrwopreglem5  30804  frgrwopreglem5ALT  30805  mdexchi  32819  atomli  32866  mdsymlem5  32891  sumdmdlem  32902  dfimafnf  33112  bnj517  35397  bnj1118  35496  mclsind  36152  dfon2lem6  36368  btwnconn1lem11  36680  finminlem  36940  isbasisrelowllem1  38112  isbasisrelowllem2  38113  poimirlem27  38399  itg2addnc  38426  rngoueqz  38693  dmncan1  38829  disjlem19  39655  lshpdisj  39863  2at0mat0  40401  llncvrlpln2  40433  lplncvrlvol2  40491  pmaple  40637  lhpexle2lem  40885  cdlemk33N  41785  cdlemk34  41786  sn-sup3d  43383  eldioph2  43610  cantnfresb  44168  gneispacess2  44989  sge0iunmpt  47249  funressnfv  47934  dfaimafn  48056  otiunsndisjX  48170  elfz2z  48206  iccelpart  48336  icceuelpart  48339  fargshiftfva  48346  sprsymrelfo  48400  sbcpr  48424  bgoldbtbndlem4  48727  grimcnv  48807  grimco  48808  clnbgrgrim  48853  uspgrlimlem4  48910  grlicsym  48932  grlictr  48934  pgnbgreunbgrlem3  49037  pgnbgreunbgrlem6  49043  idomcanl  49265  snlindsntor  49404  ldepspr  49406  nn0sumshdiglemB  49553