Theorem imp4a 426

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  imp4d  428  imp55  446  imp511  447  reuss2  4276  wefrc  5637  f1oweALT  7948  tfrlem9  8350  tz7.49  8410  oaordex  8521  dfac2b  10081  zorn2lem4  10450  zorn2lem7  10453  psslinpr  10983  facwordi  14296  ndvdssub  16434  pmtrfrn  19489  elcls  23121  elcls3  23131  neibl  24549  met2ndc  24571  itgcn  25895  branmfn  32265  atcvatlem  32545  atcvat4i  32557  umgr2cycllem  35451  satfv0fun  35682  prtlem15  39460  cvlsupr4  39930  cvlsupr5  39931  cvlsupr6  39932  2llnneN  39994  cvrat4  40028  llnexchb2  40454  cdleme48gfv1  41121  cdlemg6e  41207  dihord6apre  41841  dihord5b  41844  dihord5apre  41847  dihglblem5apreN  41876  dihglbcpreN  41885