Theorem syl2and 609

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 606	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜂))
5	1, 4	syland 604	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  610  ax7  2018  dffi3  9344  cflim2  10185  axpre-sup  11092  xle2add  13211  fzen  13495  rpmulgcd2  16625  pcqmul  16824  sbcie2s  17131  initoeu1  17978  termoeu1  17985  plttr  18306  pospo  18309  lublecllem  18324  latjlej12  18421  latmlem12  18437  hausnei2  23318  uncmp  23368  itgsubst  26016  mpodvdsmulf1o  27157  dvdsmulf1o  27159  2sqlem8a  27388  precsexlem10  28208  axcontlem9  29041  uspgr2wlkeq  29714  shintcli  31400  cvntr  32363  cdj3i  32512  f1resrcmplf1dlem  35229  satffunlem  35583  bj-bary1  37626  heicant  37976  itg2addnc  37995  dihmeetlem1N  41736  modelaxreplem1  45405  fmtnofac2lem  48025  2itscp  49251  mofsn  49313