Theorem syl2and 485

Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.)

Hypotheses

Ref	Expression
syl2and.1	|- ( ph -> ( ps -> ch ) )
syl2and.2	|- ( ph -> ( th -> ta ) )
syl2and.3	|- ( ph -> ( ( ch /\ ta ) -> et ) )

Assertion

Ref	Expression
syl2and	|- ( ph -> ( ( ps /\ th ) -> et ) )

Proof of Theorem syl2and

Step	Hyp	Ref	Expression
1		syl2and.1	. 2 |- ( ph -> ( ps -> ch ) )
2		syl2and.2	. . 3 |- ( ph -> ( th -> ta ) )
3		syl2and.3	. . 3 |- ( ph -> ( ( ch /\ ta ) -> et ) )
4	2, 3	sylan2d 484	. 2 |- ( ph -> ( ( ch /\ th ) -> et ) )
5	1, 4	syland 483	1 |- ( ph -> ( ( ps /\ th ) -> et ) )

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  anim12d  565  dffi3  7942  cflim2  8682  axpre-sup  9582  xle2add  11534  fzen  11803  rpmulgcd2  14622  pcqmul  14755  initoeu1  15850  termoeu1  15857  plttr  16160  pospo  16163  lublecllem  16178  latjlej12  16257  latmlem12  16273  cygabl  17453  hausnei2  20293  uncmp  20342  itgsubst  22895  dvdsmulf1o  24012  2sqlem8a  24188  axcontlem9  24874  usg2wotspth  25483  numclwlk1lem2f1  25693  shintcli  26843  cvntr  27806  cdj3i  27955  bj-bary1  31488  heicant  31708  itg2addnc  31729  dihmeetlem1N  34596