Theorem imp4a 422

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  imp4d  424  imp55  442  imp511  443  reuss2  4345  wefrc  5694  f1oweALT  8013  tfrlem9  8441  tz7.49  8501  oaordex  8614  dfac2b  10200  zorn2lem4  10568  zorn2lem7  10571  psslinpr  11100  facwordi  14338  ndvdssub  16457  pmtrfrn  19500  elcls  23102  elcls3  23112  neibl  24535  met2ndc  24557  itgcn  25900  branmfn  32137  atcvatlem  32417  atcvat4i  32429  umgr2cycllem  35108  satfv0fun  35339  prtlem15  38831  cvlsupr4  39301  cvlsupr5  39302  cvlsupr6  39303  2llnneN  39366  cvrat4  39400  llnexchb2  39826  cdleme48gfv1  40493  cdlemg6e  40579  dihord6apre  41213  dihord5b  41216  dihord5apre  41219  dihglblem5apreN  41248  dihglbcpreN  41257