Theorem imp4a 427

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  imp4d  429  imp55  447  imp511  448  reuss2  4218  wefrc  5519  f1oweALT  7678  tfrlem9  8032  tz7.49  8092  oaordex  8195  dfac2b  9583  zorn2lem4  9952  zorn2lem7  9955  psslinpr  10484  facwordi  13692  ndvdssub  15803  pmtrfrn  18646  elcls  21766  elcls3  21776  neibl  23196  met2ndc  23218  itgcn  24537  branmfn  29980  atcvatlem  30260  atcvat4i  30272  umgr2cycllem  32611  satfv0fun  32842  prtlem15  36444  cvlsupr4  36914  cvlsupr5  36915  cvlsupr6  36916  2llnneN  36978  cvrat4  37012  llnexchb2  37438  cdleme48gfv1  38105  cdlemg6e  38191  dihord6apre  38825  dihord5b  38828  dihord5apre  38831  dihglblem5apreN  38860  dihglbcpreN  38869