Theorem imp31 447

Description: An importation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
impd.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
imp31	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem imp31

Step	Hyp	Ref	Expression
1		impd.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	imp 444	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
3	2	imp 444	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  imp41  617  imp5d  623  impl  648  anassrs  678  an31s  844  3imp  1249  3expa  1257  reusv3  4802  otiunsndisj  4905  pwssun  4944  fri  5000  predpo  5615  ordelord  5662  tz7.7  5666  dfimafn  6155  funimass4  6157  funimass3  6241  isomin  6487  isopolem  6495  onint  6887  limsssuc  6942  tfindsg  6952  findsg  6985  suppfnss  7207  smores2  7338  tfrlem9  7368  tz7.49  7427  oecl  7504  oaordi  7513  oaass  7528  omordi  7533  odi  7546  oen0  7553  nnaordi  7585  nnmordi  7598  php3  8031  domunfican  8118  dfac5  8834  cofsmo  8974  cfcoflem  8977  zorn2lem7  9207  tskwun  9485  mulcanpi  9601  ltexprlem7  9743  sup3  10859  elnnz  11264  nzadd  11302  irradd  11688  irrmul  11689  uzsubsubfz  12234  fzo1fzo0n0  12386  elincfzoext  12393  elfzonelfzo  12436  uzindi  12643  ssnn0fi  12646  sqlecan  12833  wrd2ind  13329  repswccat  13383  cshwlen  13396  cshwidxmod  13400  2cshwcshw  13422  wrdl3s3  13553  lcmfunsnlem1  15188  lcmfdvdsb  15194  coprmprod  15213  unbenlem  15450  infpnlem1  15452  prmgaplem7  15599  iscatd  16157  initoeu1  16484  termoeu1  16491  dirtr  17059  telgsums  18213  psrbaglefi  19193  gsummoncoe1  19495  psgndiflemA  19766  isphld  19818  gsummatr01lem3  20282  cpmatmcllem  20342  mp2pm2mplem4  20433  chfacfisf  20478  chfacfisfcpmat  20479  cayleyhamilton1  20516  tgcl  20584  neindisj2  20737  2ndcdisj  21069  fgcl  21492  rnelfm  21567  alexsubALTlem3  21663  usgraexmpledg  25932  usgrares1  25939  usgrafis  25944  nbgraf1olem5  25974  nbcusgra  25992  cusgrares  26001  cusgrasize  26006  usgrwlknloop  26093  pthdepisspth  26104  usgra2adedgspthlem2  26140  usgra2wlkspth  26149  fargshiftfva  26167  usgrcyclnl2  26169  wwlkextinj  26258  wwlkextproplem2  26270  clwlkisclwwlklem2a  26313  clwlkisclwwlklem1  26315  clwwlkf1  26324  clwlkfclwwlk  26371  el2spthonot  26397  2spontn0vne  26414  eupatrl  26495  frgra3vlem1  26527  3vfriswmgralem  26531  vdgn0frgrav2  26551  vdgn1frgrav2  26553  frgrancvvdeqlemC  26566  frgrancvvdgeq  26570  frgrawopreglem5  26575  frg2woteq  26587  usg2spot2nb  26592  2spotmdisj  26595  extwwlkfablem2  26605  numclwwlkovf2ex  26613  mdexchi  28578  atomli  28625  mdsymlem5  28650  sumdmdlem  28661  dfimafnf  28817  bnj517  30209  bnj1118  30306  mclsind  30721  dfon2lem6  30937  btwnconn1lem11  31374  finminlem  31482  isbasisrelowllem1  32379  isbasisrelowllem2  32380  poimirlem27  32606  itg2addnc  32634  rngoueqz  32909  dmncan1  33045  lshpdisj  33292  2at0mat0  33829  llncvrlpln2  33861  lplncvrlvol2  33919  lhpexle2lem  34313  cdlemk33N  35215  cdlemk34  35216  eldioph2  36343  gneispacess2  37464  sge0iunmpt  39311  funressnfv  39857  dfaimafn  39894  iccelpart  39971  icceuelpart  39974  bgoldbtbndlem4  40224  otiunsndisjX  40317  elfz2z  40352  usgrexmpledg  40486  cusgrsize  40670  uspgr2wlkeqi  40856  usgr2pthlem  40969  crctcsh1wlkn0  41024  wwlksnextinj  41105  wwlksnextproplem2  41116  clwlkclwwlklem2a  41207  clwlkclwwlklem2  41209  clwwlksf1  41224  clwwlksext2edg  41230  frgr3vlem1  41443  3vfriswmgrlem  41447  vdgn1frgrv2  41466  frgrncvvdeqlemC  41478  frgrwopreglem5  41485  2wspmdisj  41501  av-numclwwlkovf2ex  41517  zrtermorngc  41793  zrtermoringc  41862  snlindsntor  42054  ldepspr  42056  nn0sumshdiglemB  42212