Theorem syl2and 601

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  anim12d  602  ax7  2063  dffi3  8625  cflim2  9420  axpre-sup  10326  xle2add  12401  fzen  12675  rpmulgcd2  15775  pcqmul  15962  initoeu1  17046  termoeu1  17053  plttr  17356  pospo  17359  lublecllem  17374  latjlej12  17453  latmlem12  17469  cygabl  18678  hausnei2  21565  uncmp  21615  itgsubst  24249  dvdsmulf1o  25372  2sqlem8a  25602  axcontlem9  26321  uspgr2wlkeq  26993  shintcli  28760  cvntr  29723  cdj3i  29872  bj-bary1  33760  heicant  34070  itg2addnc  34089  dihmeetlem1N  37444  fmtnofac2lem  42501  2itscp  43517