Theorem syl2and 500

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

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  anim12d  586  ax7  1943  dffi3  8337  cflim2  9085  axpre-sup  9990  xle2add  12089  fzen  12358  rpmulgcd2  15370  pcqmul  15558  initoeu1  16661  termoeu1  16668  plttr  16970  pospo  16973  lublecllem  16988  latjlej12  17067  latmlem12  17083  cygabl  18292  hausnei2  21157  uncmp  21206  itgsubst  23812  dvdsmulf1o  24920  2sqlem8a  25150  axcontlem9  25852  uspgr2wlkeq  26542  numclwlk1lem2f1  27227  shintcli  28188  cvntr  29151  cdj3i  29300  bj-bary1  33162  heicant  33444  itg2addnc  33464  dihmeetlem1N  36579  fmtnofac2lem  41480