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  4275  wefrc  5615  f1oweALT  7913  tfrlem9  8313  tz7.49  8373  oaordex  8482  dfac2b  10033  zorn2lem4  10401  zorn2lem7  10404  psslinpr  10933  facwordi  14203  ndvdssub  16327  pmtrfrn  19378  elcls  23008  elcls3  23018  neibl  24436  met2ndc  24458  itgcn  25793  branmfn  32106  atcvatlem  32386  atcvat4i  32398  umgr2cycllem  35256  satfv0fun  35487  prtlem15  39047  cvlsupr4  39517  cvlsupr5  39518  cvlsupr6  39519  2llnneN  39581  cvrat4  39615  llnexchb2  40041  cdleme48gfv1  40708  cdlemg6e  40794  dihord6apre  41428  dihord5b  41431  dihord5apre  41434  dihglblem5apreN  41463  dihglbcpreN  41472