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  4271  wefrc  5605  f1oweALT  7899  tfrlem9  8299  tz7.49  8359  oaordex  8468  dfac2b  10017  zorn2lem4  10385  zorn2lem7  10388  psslinpr  10917  facwordi  14191  ndvdssub  16315  pmtrfrn  19365  elcls  22983  elcls3  22993  neibl  24411  met2ndc  24433  itgcn  25768  branmfn  32077  atcvatlem  32357  atcvat4i  32369  umgr2cycllem  35176  satfv0fun  35407  prtlem15  38914  cvlsupr4  39384  cvlsupr5  39385  cvlsupr6  39386  2llnneN  39448  cvrat4  39482  llnexchb2  39908  cdleme48gfv1  40575  cdlemg6e  40661  dihord6apre  41295  dihord5b  41298  dihord5apre  41301  dihglblem5apreN  41330  dihglbcpreN  41339