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  4280  wefrc  5626  f1oweALT  7926  tfrlem9  8326  tz7.49  8386  oaordex  8495  dfac2b  10053  zorn2lem4  10421  zorn2lem7  10424  psslinpr  10954  facwordi  14224  ndvdssub  16348  pmtrfrn  19399  elcls  23029  elcls3  23039  neibl  24457  met2ndc  24479  itgcn  25814  branmfn  32193  atcvatlem  32473  atcvat4i  32485  umgr2cycllem  35356  satfv0fun  35587  prtlem15  39251  cvlsupr4  39721  cvlsupr5  39722  cvlsupr6  39723  2llnneN  39785  cvrat4  39819  llnexchb2  40245  cdleme48gfv1  40912  cdlemg6e  40998  dihord6apre  41632  dihord5b  41635  dihord5apre  41638  dihglblem5apreN  41667  dihglbcpreN  41676