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  7681  cflim2  8432  axpre-sup  9336  xle2add  11222  fzen  11467  rpmulgcd2  13791  pcqmul  13920  plttr  15140  pospo  15143  lublecllem  15158  latjlej12  15237  latmlem12  15253  cygabl  16367  hausnei2  18957  uncmp  19006  itgsubst  21521  dvdsmulf1o  22534  2sqlem8a  22710  axcontlem9  23218  shintcli  24732  cvntr  25696  cdj3i  25845  heicant  28426  itg2addnc  28446  usg2wotspth  30403  numclwlk1lem2f1  30687  bj-bary1  32601  dihmeetlem1N  34935