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

This theorem is referenced by:  imp4d  428  imp55  446  imp511  447  reuss2  4235  wefrc  5513  f1oweALT  7655  tfrlem9  8004  tz7.49  8064  oaordex  8167  dfac2b  9541  zorn2lem4  9910  zorn2lem7  9913  psslinpr  10442  facwordi  13645  ndvdssub  15750  pmtrfrn  18578  elcls  21678  elcls3  21688  neibl  23108  met2ndc  23130  itgcn  24448  branmfn  29888  atcvatlem  30168  atcvat4i  30180  umgr2cycllem  32500  satfv0fun  32731  prtlem15  36171  cvlsupr4  36641  cvlsupr5  36642  cvlsupr6  36643  2llnneN  36705  cvrat4  36739  llnexchb2  37165  cdleme48gfv1  37832  cdlemg6e  37918  dihord6apre  38552  dihord5b  38555  dihord5apre  38558  dihglblem5apreN  38587  dihglbcpreN  38596