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  9338  cflim2  10177  axpre-sup  11084  xle2add  13178  fzen  13461  rpmulgcd2  16587  pcqmul  16785  sbcie2s  17092  initoeu1  17939  termoeu1  17946  plttr  18267  pospo  18270  lublecllem  18285  latjlej12  18382  latmlem12  18398  hausnei2  23301  uncmp  23351  itgsubst  26016  mpodvdsmulf1o  27164  dvdsmulf1o  27166  2sqlem8a  27396  precsexlem10  28197  axcontlem9  29028  uspgr2wlkeq  29702  shintcli  31387  cvntr  32350  cdj3i  32499  f1resrcmplf1dlem  35223  satffunlem  35576  bj-bary1  37488  heicant  37827  itg2addnc  37846  dihmeetlem1N  41587  modelaxreplem1  45255  fmtnofac2lem  47850  2itscp  49063  mofsn  49125