Theorem imp4a 423

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  imp4d  425  imp55  443  imp511  444  reuss2  4249  wefrc  5583  f1oweALT  7815  tfrlem9  8216  tz7.49  8276  oaordex  8389  dfac2b  9886  zorn2lem4  10255  zorn2lem7  10258  psslinpr  10787  facwordi  14003  ndvdssub  16118  pmtrfrn  19066  elcls  22224  elcls3  22234  neibl  23657  met2ndc  23679  itgcn  25009  branmfn  30467  atcvatlem  30747  atcvat4i  30759  umgr2cycllem  33102  satfv0fun  33333  prtlem15  36889  cvlsupr4  37359  cvlsupr5  37360  cvlsupr6  37361  2llnneN  37423  cvrat4  37457  llnexchb2  37883  cdleme48gfv1  38550  cdlemg6e  38636  dihord6apre  39270  dihord5b  39273  dihord5apre  39276  dihglblem5apreN  39305  dihglbcpreN  39314