Theorem syld3an3 1294

Description: A syllogism inference. (Contributed by NM, 20-May-2007.)

Hypotheses

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

Assertion

Ref	Expression
syld3an3	|- ( ( ph /\ ps /\ ch ) -> ta )

Proof of Theorem syld3an3

Step	Hyp	Ref	Expression
1		simp1 999	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2		simp2 1000	. 2 |- ( ( ph /\ ps /\ ch ) -> ps )
3		syld3an3.1	. 2 |- ( ( ph /\ ps /\ ch ) -> th )
4		syld3an3.2	. 2 |- ( ( ph /\ ps /\ th ) -> ta )
5	1, 2, 3, 4	syl3anc 1249	1 |- ( ( ph /\ ps /\ ch ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  syld3an1  1295  syld3an2  1296  brelrng  4898  moriotass  5907  nnncan1  8265  lediv1  8899  modqval  10419  modqvalr  10420  modqcl  10421  flqpmodeq  10422  modq0  10424  modqge0  10427  modqlt  10428  modqdiffl  10430  modqdifz  10431  modqvalp1  10438  exp3val  10636  bcval4  10847  dvdsmultr1  11999  dvdssub2  12003  divalglemeuneg  12091  ndvdsadd  12099  grpsubf  13237  grpinvsub  13240  grpnpcan  13250  mulginvcom  13303  mulginvinv  13304  subgsubcl  13341  qussub  13393  ghmsub  13407  dvrcl  13717  unitdvcl  13718  basgen2  14343  opnneiss  14420  cnpf2  14469  sincosq1lem  15087