Theorem imp4a 423

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 422	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	ex 413	1 ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)))

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  imp4d  425  imp55  443  imp511  444  reuss2  4254  wefrc  5612  f1oweALT  7914  tfrlem9  8314  tz7.49  8374  oaordex  8483  dfac2b  10044  zorn2lem4  10412  zorn2lem7  10415  psslinpr  10945  facwordi  14242  ndvdssub  16369  pmtrfrn  19424  elcls  23056  elcls3  23066  neibl  24484  met2ndc  24506  itgcn  25830  branmfn  32194  atcvatlem  32474  atcvat4i  32486  umgr2cycllem  35368  satfv0fun  35599  prtlem15  39367  cvlsupr4  39837  cvlsupr5  39838  cvlsupr6  39839  2llnneN  39901  cvrat4  39935  llnexchb2  40361  cdleme48gfv1  41028  cdlemg6e  41114  dihord6apre  41748  dihord5b  41751  dihord5apre  41754  dihglblem5apreN  41783  dihglbcpreN  41792