Theorem syl2and 486

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

Syntax hints:   -> wi 4   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  anim12d  566  ax7  1860  dffi3  7945  cflim2  8693  axpre-sup  9593  xle2add  11545  fzen  11816  rpmulgcd2  14662  pcqmul  14803  initoeu1  15906  termoeu1  15913  plttr  16216  pospo  16219  lublecllem  16234  latjlej12  16313  latmlem12  16329  cygabl  17525  hausnei2  20369  uncmp  20418  itgsubst  23001  dvdsmulf1o  24123  2sqlem8a  24299  axcontlem9  25002  usg2wotspth  25612  numclwlk1lem2f1  25822  shintcli  26982  cvntr  27945  cdj3i  28094  bj-bary1  31717  heicant  31975  itg2addnc  31996  dihmeetlem1N  34858