Theorem syl2and 619

Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.)

Hypotheses

Ref	Expression
syl2and.1	⊢ (𝜑 → (𝜓 → 𝜒))
syl2and.2	⊢ (𝜑 → (𝜃 → 𝜏))
syl2and.3	⊢ (𝜑 → ((𝜒 ∧ 𝜏) → 𝜂))

Assertion

Ref	Expression
syl2and	⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂))

Proof of Theorem syl2and

Step	Hyp	Ref	Expression
1		syl2and.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl2and.2	. . 3 ⊢ (𝜑 → (𝜃 → 𝜏))
3		syl2and.3	. . 3 ⊢ (𝜑 → ((𝜒 ∧ 𝜏) → 𝜂))
4	2, 3	sylan2d 616	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜂))
5	1, 4	syland 614	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:  anim12d  620  ax7  2039  dffi3  9379  cflim2  10235  axpre-sup  11142  xle2add  13276  fzen  13560  rpmulgcd2  16704  pcqmul  16903  sbcie2s  17211  initoeu1  18058  termoeu1  18065  plttr  18386  pospo  18389  lublecllem  18404  latjlej12  18501  latmlem12  18517  hausnei2  23471  uncmp  23521  itgsubst  26169  mpodvdsmulf1o  27316  dvdsmulf1o  27318  2sqlem8a  27547  precsexlem10  28367  axcontlem9  29231  uspgr2wlkeq  29904  shintcli  31590  cvntr  32553  cdj3i  32702  f1resrcmplf1dlem  35390  satffunlem  35764  bj-bary1  37816  heicant  38166  itg2addnc  38185  dihmeetlem1N  41926  modelaxreplem1  45552  fmtnofac2lem  48175  2itscp  49412  mofsn  49473