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  2017  dffi3  9310  cflim2  10146  axpre-sup  11052  xle2add  13150  fzen  13433  rpmulgcd2  16559  pcqmul  16757  sbcie2s  17064  initoeu1  17910  termoeu1  17917  plttr  18238  pospo  18241  lublecllem  18256  latjlej12  18353  latmlem12  18369  hausnei2  23261  uncmp  23311  itgsubst  25976  mpodvdsmulf1o  27124  dvdsmulf1o  27126  2sqlem8a  27356  precsexlem10  28147  axcontlem9  28943  uspgr2wlkeq  29617  shintcli  31299  cvntr  32262  cdj3i  32411  f1resrcmplf1dlem  35088  satffunlem  35413  bj-bary1  37325  heicant  37674  itg2addnc  37693  dihmeetlem1N  41308  modelaxreplem1  44990  fmtnofac2lem  47578  2itscp  48792  mofsn  48854