Theorem syl2and 608

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 605	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜂))
5	1, 4	syland 603	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:  anim12d  609  ax7  2019  dffi3  9190  cflim2  10019  axpre-sup  10925  xle2add  12993  fzen  13273  rpmulgcd2  16361  pcqmul  16554  initoeu1  17726  termoeu1  17733  plttr  18060  pospo  18063  lublecllem  18078  latjlej12  18173  latmlem12  18189  cygablOLD  19492  hausnei2  22504  uncmp  22554  itgsubst  25213  dvdsmulf1o  26343  2sqlem8a  26573  axcontlem9  27340  uspgr2wlkeq  28013  shintcli  29691  cvntr  30654  cdj3i  30803  f1resrcmplf1dlem  33058  satffunlem  33363  bj-bary1  35483  heicant  35812  itg2addnc  35831  dihmeetlem1N  39304  fmtnofac2lem  45020  2itscp  46127  mofsn  46171