Theorem syl2and 499

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 498	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜂))
5	1, 4	syland 497	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂))

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  anim12d  584  ax7  1930  dffi3  8220  cflim2  8968  axpre-sup  9869  xle2add  11961  fzen  12229  rpmulgcd2  15208  pcqmul  15396  initoeu1  16484  termoeu1  16491  plttr  16793  pospo  16796  lublecllem  16811  latjlej12  16890  latmlem12  16906  cygabl  18115  hausnei2  20967  uncmp  21016  itgsubst  23616  dvdsmulf1o  24720  2sqlem8a  24950  axcontlem9  25652  usg2wotspth  26411  numclwlk1lem2f1  26621  shintcli  27572  cvntr  28535  cdj3i  28684  bj-bary1  32339  heicant  32614  itg2addnc  32634  dihmeetlem1N  35597  fmtnofac2lem  40018  uspgr2wlkeq  40854  av-numclwlk1lem2f1  41524