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 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:  anim12d  609  ax7  2012  dffi3  9468  cflim2  10300  axpre-sup  11206  xle2add  13297  fzen  13577  rpmulgcd2  16689  pcqmul  16886  sbcie2s  17194  initoeu1  18064  termoeu1  18071  plttr  18399  pospo  18402  lublecllem  18417  latjlej12  18512  latmlem12  18528  hausnei2  23376  uncmp  23426  itgsubst  26104  mpodvdsmulf1o  27251  dvdsmulf1o  27253  2sqlem8a  27483  precsexlem10  28254  axcontlem9  29001  uspgr2wlkeq  29678  shintcli  31357  cvntr  32320  cdj3i  32469  f1resrcmplf1dlem  35078  satffunlem  35385  bj-bary1  37294  heicant  37641  itg2addnc  37660  dihmeetlem1N  41272  modelaxreplem1  44942  fmtnofac2lem  47492  2itscp  48630  mofsn  48673