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  4272  wefrc  5645  f1oweALT  7982  tfrlem9  8386  tz7.49  8448  oaordex  8559  dfac2b  10202  zorn2lem4  10570  zorn2lem7  10573  psslinpr  11109  facwordi  14426  ndvdssub  16572  pmtrfrn  19665  elcls  23384  elcls3  23394  neibl  24813  met2ndc  24835  itgcn  26158  umgr2cycllem  30739  branmfn  32700  atcvatlem  32980  atcvat4i  32992  satfv0fun  36115  prtlem15  39912  cvlsupr4  40382  cvlsupr5  40383  cvlsupr6  40384  2llnneN  40446  cvrat4  40480  llnexchb2  40906  cdleme48gfv1  41573  cdlemg6e  41659  dihord6apre  42293  dihord5b  42296  dihord5apre  42299  dihglblem5apreN  42328  dihglbcpreN  42337