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  4282  wefrc  5660  f1oweALT  7978  tfrlem9  8381  tz7.49  8441  oaordex  8552  dfac2b  10133  zorn2lem4  10501  zorn2lem7  10504  psslinpr  11034  facwordi  14345  ndvdssub  16492  pmtrfrn  19559  elcls  23267  elcls3  23277  neibl  24695  met2ndc  24717  itgcn  26041  branmfn  32494  atcvatlem  32774  atcvat4i  32786  umgr2cycllem  35652  satfv0fun  35883  prtlem15  39689  cvlsupr4  40159  cvlsupr5  40160  cvlsupr6  40161  2llnneN  40223  cvrat4  40257  llnexchb2  40683  cdleme48gfv1  41350  cdlemg6e  41436  dihord6apre  42070  dihord5b  42073  dihord5apre  42076  dihglblem5apreN  42105  dihglbcpreN  42114