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  4280  wefrc  5632  f1oweALT  7910  tfrlem9  8336  tz7.49  8396  oaordex  8510  dfac2b  10075  zorn2lem4  10444  zorn2lem7  10447  psslinpr  10976  facwordi  14199  ndvdssub  16302  pmtrfrn  19254  elcls  22461  elcls3  22471  neibl  23894  met2ndc  23916  itgcn  25246  branmfn  31110  atcvatlem  31390  atcvat4i  31402  umgr2cycllem  33821  satfv0fun  34052  prtlem15  37410  cvlsupr4  37880  cvlsupr5  37881  cvlsupr6  37882  2llnneN  37945  cvrat4  37979  llnexchb2  38405  cdleme48gfv1  39072  cdlemg6e  39158  dihord6apre  39792  dihord5b  39795  dihord5apre  39798  dihglblem5apreN  39827  dihglbcpreN  39836