Theorem imp4a 425

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 424	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	ex 415	1 ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  imp4d  427  imp55  445  imp511  446  reuss2  4286  wefrc  5552  f1oweALT  7676  tfrlem9  8024  tz7.49  8084  oaordex  8187  dfac2b  9559  zorn2lem4  9924  zorn2lem7  9927  psslinpr  10456  facwordi  13652  ndvdssub  15763  pmtrfrn  18589  elcls  21684  elcls3  21694  neibl  23114  met2ndc  23136  itgcn  24446  branmfn  29885  atcvatlem  30165  atcvat4i  30177  umgr2cycllem  32391  satfv0fun  32622  prtlem15  36015  cvlsupr4  36485  cvlsupr5  36486  cvlsupr6  36487  2llnneN  36549  cvrat4  36583  llnexchb2  37009  cdleme48gfv1  37676  cdlemg6e  37762  dihord6apre  38396  dihord5b  38399  dihord5apre  38402  dihglblem5apreN  38431  dihglbcpreN  38440