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  4301  wefrc  5648  f1oweALT  7971  tfrlem9  8399  tz7.49  8459  oaordex  8570  dfac2b  10145  zorn2lem4  10513  zorn2lem7  10516  psslinpr  11045  facwordi  14307  ndvdssub  16428  pmtrfrn  19439  elcls  23011  elcls3  23021  neibl  24440  met2ndc  24462  itgcn  25798  branmfn  32086  atcvatlem  32366  atcvat4i  32378  umgr2cycllem  35162  satfv0fun  35393  prtlem15  38893  cvlsupr4  39363  cvlsupr5  39364  cvlsupr6  39365  2llnneN  39428  cvrat4  39462  llnexchb2  39888  cdleme48gfv1  40555  cdlemg6e  40641  dihord6apre  41275  dihord5b  41278  dihord5apre  41281  dihglblem5apreN  41310  dihglbcpreN  41319