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  2016  dffi3  9340  cflim2  10176  axpre-sup  11082  xle2add  13179  fzen  13462  rpmulgcd2  16585  pcqmul  16783  sbcie2s  17090  initoeu1  17936  termoeu1  17943  plttr  18264  pospo  18267  lublecllem  18282  latjlej12  18379  latmlem12  18395  hausnei2  23256  uncmp  23306  itgsubst  25972  mpodvdsmulf1o  27120  dvdsmulf1o  27122  2sqlem8a  27352  precsexlem10  28141  axcontlem9  28935  uspgr2wlkeq  29609  shintcli  31291  cvntr  32254  cdj3i  32403  f1resrcmplf1dlem  35052  satffunlem  35373  bj-bary1  37285  heicant  37634  itg2addnc  37653  dihmeetlem1N  41269  modelaxreplem1  44952  fmtnofac2lem  47553  2itscp  48754  mofsn  48816