Theorem syl2and 616

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 613	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜂))
5	1, 4	syland 611	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anim12d  617  ax7  2030  dffi3  9367  cflim2  10210  axpre-sup  11117  xle2add  13252  fzen  13536  rpmulgcd2  16666  pcqmul  16865  sbcie2s  17173  initoeu1  18020  termoeu1  18027  plttr  18348  pospo  18351  lublecllem  18366  latjlej12  18463  latmlem12  18479  hausnei2  23386  uncmp  23436  itgsubst  26084  mpodvdsmulf1o  27228  dvdsmulf1o  27230  2sqlem8a  27459  precsexlem10  28279  axcontlem9  29112  uspgr2wlkeq  29785  shintcli  31471  cvntr  32434  cdj3i  32583  f1resrcmplf1dlem  35337  satffunlem  35699  bj-bary1  37752  heicant  38102  itg2addnc  38121  dihmeetlem1N  41862  modelaxreplem1  45502  fmtnofac2lem  48125  2itscp  49351  mofsn  49413