Theorem syl2and 483

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 482	. 2 |- ( ph -> ( ( ch /\ th ) -> et ) )
5	1, 4	syland 481	1 |- ( ph -> ( ( ps /\ th ) -> et ) )

Syntax hints:   -> wi 4   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  anim12d  563  dffi3  7892  cflim2  8644  axpre-sup  9547  xle2add  11452  fzen  11704  rpmulgcd2  14108  pcqmul  14239  plttr  15460  pospo  15463  lublecllem  15478  latjlej12  15557  latmlem12  15573  cygabl  16708  hausnei2  19660  uncmp  19709  itgsubst  22277  dvdsmulf1o  23295  2sqlem8a  23471  axcontlem9  24048  usg2wotspth  24657  numclwlk1lem2f1  24868  shintcli  26020  cvntr  26984  cdj3i  27133  heicant  29902  itg2addnc  29922  bj-bary1  33970  dihmeetlem1N  36304