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  9325  cflim2  10164  axpre-sup  11070  xle2add  13168  fzen  13451  rpmulgcd2  16577  pcqmul  16775  sbcie2s  17082  initoeu1  17928  termoeu1  17935  plttr  18256  pospo  18259  lublecllem  18274  latjlej12  18371  latmlem12  18387  hausnei2  23278  uncmp  23328  itgsubst  25993  mpodvdsmulf1o  27141  dvdsmulf1o  27143  2sqlem8a  27373  precsexlem10  28164  axcontlem9  28961  uspgr2wlkeq  29635  shintcli  31320  cvntr  32283  cdj3i  32432  f1resrcmplf1dlem  35109  satffunlem  35456  bj-bary1  37367  heicant  37705  itg2addnc  37724  dihmeetlem1N  41399  modelaxreplem1  45085  fmtnofac2lem  47682  2itscp  48896  mofsn  48958