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  5496  pwssun  5546  ordelord  6390  tz7.7  6394  dfimafn  6955  funimass4  6957  funimass3  7061  isomin  7352  isopolem  7360  onint  7811  limsssuc  7868  tfindsg  7879  findsg  7916  suppfnss  8217  smores2  8373  tfrlem9  8404  tz7.49  8466  oecl  8556  oaordi  8565  oaass  8580  omordi  8585  odi  8598  oen0  8606  nnaordi  8638  nnmordi  8651  domunfican  9324  dfac5  10217  cofsmo  10357  cfcoflem  10360  zorn2lem7  10590  tskwun  10879  mulcanpi  10995  ltexprlem7  11137  sup3  12284  elnnz  12713  nzadd  12754  irradd  13111  irrmul  13112  uzsubsubfz  13690  fzo1fzo0n0  13860  elincfzoext  13868  elfzonelfzo  13914  uzindi  14135  ssnn0fi  14138  sqlecan  14363  swrdnd2  14816  swrdwrdsymb  14823  wrd2ind  14883  repswccat  14948  cshwlen  14961  cshwidxmod  14965  2cshwcshw  14987  wrdl3s3  15127  lcmfunsnlem1  16824  coprmprod  16848  unbenlem  17098  infpnlem1  17100  prmgaplem7  17247  iscatd  17859  dirtr  18788  telgsums  20219  zrtermorngc  20907  zrtermoringc  20939  prmidlc  21641  psgndiflemA  21919  isphld  21972  gsummoncoe1  22638  gsummatr01lem3  22984  cpmatmcllem  23048  mp2pm2mplem4  23139  chfacfisf  23184  chfacfisfcpmat  23185  cayleyhamilton1  23222  tgcl  23299  neindisj2  23453  2ndcdisj  23787  fgcl  24209  rnelfm  24284  alexsubALTlem3  24380  2sqreultlem  27786  2sqreunnltlem  27789  elnnzs  28799  usgrexmpledg  29855  cusgrsize  30047  uspgr2wlkeqi  30240  usgr2wlkneq  30354  usgr2pthlem  30361  crctcshwlkn0  30422  wwlksnextinj  30500  wwlksnextproplem2  30511  wwlksnextproplem3  30512  clwlkclwwlklem2a  30601  clwlkclwwlklem2  30603  clwwlkf1  30652  clwwlknwwlksnb  30658  clwwlkext2edg  30659  clwwlknonex2lem2  30711  frgr3vlem1  30886  3vfriswmgrlem  30890  vdgn1frgrv2  30909  frgrwopreglem5  30934  frgrwopreglem5ALT  30935  mdexchi  32949  atomli  32996  mdsymlem5  33021  sumdmdlem  33032  dfimafnf  33284  bnj517  35568  bnj1118  35667  mclsind  36456  dfon2lem6  36677  btwnconn1lem11  36989  finminlem  37233  isbasisrelowllem1  38418  isbasisrelowllem2  38419  poimirlem27  38705  itg2addnc  38732  rngoueqz  39014  dmncan1  39150  disjlem19  39976  lshpdisj  40184  2at0mat0  40722  llncvrlpln2  40754  lplncvrlvol2  40812  pmaple  40958  lhpexle2lem  41206  cdlemk33N  42106  cdlemk34  42107  sn-sup3d  43696  eldioph2  43913  cantnfresb  44466  gneispacess2  45286  sge0iunmpt  47567  funressnfv  48252  dfaimafn  48374  otiunsndisjX  48488  elfz2z  48524  iccelpart  48654  icceuelpart  48657  fargshiftfva  48664  sprsymrelfo  48718  sbcpr  48742  bgoldbtbndlem4  49045  grimcnv  49125  grimco  49126  clnbgrgrim  49171  uspgrlimlem4  49228  grlicsym  49250  grlictr  49252  pgnbgreunbgrlem3  49355  pgnbgreunbgrlem6  49361  idomcanl  49583  snlindsntor  49722  ldepspr  49724  nn0sumshdiglemB  49871