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  4332  wefrc  5683  f1oweALT  7996  tfrlem9  8424  tz7.49  8484  oaordex  8595  dfac2b  10169  zorn2lem4  10537  zorn2lem7  10540  psslinpr  11069  facwordi  14325  ndvdssub  16443  pmtrfrn  19491  elcls  23097  elcls3  23107  neibl  24530  met2ndc  24552  itgcn  25895  branmfn  32134  atcvatlem  32414  atcvat4i  32426  umgr2cycllem  35125  satfv0fun  35356  prtlem15  38857  cvlsupr4  39327  cvlsupr5  39328  cvlsupr6  39329  2llnneN  39392  cvrat4  39426  llnexchb2  39852  cdleme48gfv1  40519  cdlemg6e  40605  dihord6apre  41239  dihord5b  41242  dihord5apre  41245  dihglblem5apreN  41274  dihglbcpreN  41283