Theorem imp4a 428

Description: An importation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Jul-2021.)

Hypothesis

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

Assertion

Ref	Expression
imp4a	⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)))

Proof of Theorem imp4a

Step	Hyp	Ref	Expression
1		imp4.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	imp4b 427	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	ex 418	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:  imp4d  430  imp55  448  imp511  449  reuss2  4272  wefrc  5649  f1oweALT  7969  tfrlem9  8374  tz7.49  8434  oaordex  8545  dfac2b  10133  zorn2lem4  10501  zorn2lem7  10504  psslinpr  11040  facwordi  14353  ndvdssub  16499  pmtrfrn  19585  elcls  23298  elcls3  23308  neibl  24727  met2ndc  24749  itgcn  26072  umgr2cycllem  30625  branmfn  32586  atcvatlem  32866  atcvat4i  32878  satfv0fun  35950  prtlem15  39748  cvlsupr4  40218  cvlsupr5  40219  cvlsupr6  40220  2llnneN  40282  cvrat4  40316  llnexchb2  40742  cdleme48gfv1  41409  cdlemg6e  41495  dihord6apre  42129  dihord5b  42132  dihord5apre  42135  dihglblem5apreN  42164  dihglbcpreN  42173