Theorem imp31 422

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

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

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 401

This theorem is used by:  imp41  430  imp5d  444  impl  460  anassrs  472  an31s  666  3imp  1127  reusv3  5375  otiunsndisj  5502  pwssun  5552  ordelord  6382  tz7.7  6386  dfimafn  6943  funimass4  6945  funimass3  7049  isomin  7335  isopolem  7343  onint  7787  limsssuc  7844  tfindsg  7855  findsg  7892  suppfnss  8183  smores2  8339  tfrlem9  8370  tz7.49  8430  oecl  8520  oaordi  8529  oaass  8544  omordi  8549  odi  8562  oen0  8570  nnaordi  8602  nnmordi  8615  domunfican  9279  dfac5  10119  cofsmo  10259  cfcoflem  10262  zorn2lem7  10492  tskwun  10775  mulcanpi  10891  ltexprlem7  11033  sup3  12178  elnnz  12607  nzadd  12648  irradd  13003  irrmul  13004  uzsubsubfz  13581  fzo1fzo0n0  13751  elincfzoext  13759  elfzonelfzo  13805  uzindi  14025  ssnn0fi  14028  sqlecan  14252  swrdnd2  14700  swrdwrdsymb  14707  wrd2ind  14767  repswccat  14830  cshwlen  14843  cshwidxmod  14847  2cshwcshw  14869  wrdl3s3  15006  lcmfunsnlem1  16701  coprmprod  16725  unbenlem  16974  infpnlem1  16976  prmgaplem7  17123  iscatd  17735  dirtr  18664  telgsums  20069  zrtermorngc  20753  zrtermoringc  20785  prmidlc  21484  psgndiflemA  21762  isphld  21815  gsummoncoe1  22479  gsummatr01lem3  22825  cpmatmcllem  22886  mp2pm2mplem4  22977  chfacfisf  23022  chfacfisfcpmat  23023  cayleyhamilton1  23060  tgcl  23137  neindisj2  23291  2ndcdisj  23624  fgcl  24046  rnelfm  24121  alexsubALTlem3  24217  2sqreultlem  27622  2sqreunnltlem  27625  elnnzs  28605  usgrexmpledg  29623  cusgrsize  29815  uspgr2wlkeqi  30008  usgr2wlkneq  30116  usgr2pthlem  30123  crctcshwlkn0  30181  wwlksnextinj  30259  wwlksnextproplem2  30270  wwlksnextproplem3  30271  clwlkclwwlklem2a  30360  clwlkclwwlklem2  30362  clwwlkf1  30411  clwwlknwwlksnb  30417  clwwlkext2edg  30418  clwwlknonex2lem2  30470  frgr3vlem1  30635  3vfriswmgrlem  30639  vdgn1frgrv2  30658  frgrwopreglem5  30683  frgrwopreglem5ALT  30684  mdexchi  32698  atomli  32745  mdsymlem5  32770  sumdmdlem  32781  dfimafnf  32992  bnj517  35282  bnj1118  35381  mclsind  36070  dfon2lem6  36286  btwnconn1lem11  36597  finminlem  36857  isbasisrelowllem1  38029  isbasisrelowllem2  38030  poimirlem27  38326  itg2addnc  38353  rngoueqz  38619  dmncan1  38755  disjlem19  39581  lshpdisj  39789  2at0mat0  40327  llncvrlpln2  40359  lplncvrlvol2  40417  pmaple  40563  lhpexle2lem  40811  cdlemk33N  41711  cdlemk34  41712  sn-sup3d  43294  eldioph2  43521  cantnfresb  44079  gneispacess2  44900  sge0iunmpt  47160  funressnfv  47808  dfaimafn  47930  otiunsndisjX  48044  elfz2z  48080  iccelpart  48210  icceuelpart  48213  fargshiftfva  48220  sprsymrelfo  48274  sbcpr  48298  bgoldbtbndlem4  48601  grimcnv  48681  grimco  48682  clnbgrgrim  48727  uspgrlimlem4  48784  grlicsym  48806  grlictr  48808  pgnbgreunbgrlem3  48911  pgnbgreunbgrlem6  48917  idomcanl  49140  snlindsntor  49279  ldepspr  49281  nn0sumshdiglemB  49428