Theorem syl31anc 1231

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
sylXanc.1	|- ( ph -> ps )
sylXanc.2	|- ( ph -> ch )
sylXanc.3	|- ( ph -> th )
sylXanc.4	|- ( ph -> ta )
syl31anc.5	|- ( ( ( ps /\ ch /\ th ) /\ ta ) -> et )

Assertion

Ref	Expression
syl31anc	|- ( ph -> et )

Proof of Theorem syl31anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 |- ( ph -> ps )
2		sylXanc.2	. . 3 |- ( ph -> ch )
3		sylXanc.3	. . 3 |- ( ph -> th )
4	1, 2, 3	3jca 1167	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
5		sylXanc.4	. 2 |- ( ph -> ta )
6		syl31anc.5	. 2 |- ( ( ( ps /\ ch /\ th ) /\ ta ) -> et )
7	4, 5, 6	syl2anc 409	1 |- ( ph -> et )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 968

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

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  syl32anc  1236  stoic4b  1421  enq0tr  7375  ltmul12a  8755  lt2msq1  8780  ledivp1  8798  lemul1ad  8834  lemul2ad  8835  lediv2ad  9655  xaddge0  9814  difelfznle  10070  expubnd  10512  nn0leexp2  10624  expcanlem  10628  expcand  10630  xrmaxaddlem  11201  mertenslemi1  11476  eftlub  11631  dvdsadd  11776  divalgmod  11864  gcdzeq  11955  rplpwr  11960  sqgcd  11962  bezoutr  11965  rpmulgcd2  12027  rpdvds  12031  isprm5  12074  divgcdodd  12075  oddpwdclemxy  12101  divnumden  12128  crth  12156  phimullem  12157  coprimeprodsq2  12190  pythagtriplem19  12214  pclemub  12219  pcpre1  12224  pcidlem  12254  pockthlem  12286  prmunb  12292  xblss2ps  13044  xblss2  13045  metcnpi3  13157  limcimolemlt  13273  limccnp2cntop  13286  dvmulxxbr  13306  dvcoapbr  13311  2sqlem8a  13598  2sqlem8  13599