Theorem syl2and 607

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 604	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜂))
5	1, 4	syland 602	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 206  df-an 396

This theorem is referenced by:  anim12d  608  ax7  2012  dffi3  9446  cflim2  10278  axpre-sup  11184  xle2add  13262  fzen  13542  rpmulgcd2  16618  pcqmul  16813  sbcie2s  17121  initoeu1  17991  termoeu1  17998  plttr  18325  pospo  18328  lublecllem  18343  latjlej12  18438  latmlem12  18454  hausnei2  23244  uncmp  23294  itgsubst  25971  mpodvdsmulf1o  27113  dvdsmulf1o  27115  2sqlem8a  27345  precsexlem10  28101  axcontlem9  28770  uspgr2wlkeq  29447  shintcli  31126  cvntr  32089  cdj3i  32238  f1resrcmplf1dlem  34645  satffunlem  34947  bj-bary1  36727  heicant  37063  itg2addnc  37082  dihmeetlem1N  40700  fmtnofac2lem  46831  2itscp  47777  mofsn  47819