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  4266  wefrc  5625  f1oweALT  7925  tfrlem9  8324  tz7.49  8384  oaordex  8493  dfac2b  10053  zorn2lem4  10421  zorn2lem7  10424  psslinpr  10954  facwordi  14251  ndvdssub  16378  pmtrfrn  19433  elcls  23038  elcls3  23048  neibl  24466  met2ndc  24488  itgcn  25812  branmfn  32176  atcvatlem  32456  atcvat4i  32468  umgr2cycllem  35322  satfv0fun  35553  prtlem15  39321  cvlsupr4  39791  cvlsupr5  39792  cvlsupr6  39793  2llnneN  39855  cvrat4  39889  llnexchb2  40315  cdleme48gfv1  40982  cdlemg6e  41068  dihord6apre  41702  dihord5b  41705  dihord5apre  41708  dihglblem5apreN  41737  dihglbcpreN  41746