Theorem syl31anc 1252

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 1179	. 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 411	1 |- ( ph -> et )

Syntax hints:   -> wi 4   /\ wa 104   /\ 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:  syl32anc  1257  stoic4b  1444  enq0tr  7464  ltmul12a  8848  lt2msq1  8873  ledivp1  8891  lemul1ad  8927  lemul2ad  8928  lediv2ad  9751  xaddge0  9910  difelfznle  10167  expubnd  10611  nn0leexp2  10725  expcanlem  10730  expcand  10732  xrmaxaddlem  11303  mertenslemi1  11578  eftlub  11733  dvdsadd  11878  divalgmod  11967  gcdzeq  12058  rplpwr  12063  sqgcd  12065  bezoutr  12068  rpmulgcd2  12130  rpdvds  12134  isprm5  12177  divgcdodd  12178  oddpwdclemxy  12204  divnumden  12231  crth  12259  phimullem  12260  coprimeprodsq2  12293  pythagtriplem19  12317  pclemub  12322  pcpre1  12327  pcidlem  12358  pockthlem  12391  prmunb  12397  kerf1ghm  13230  elrhmunit  13544  xblss2ps  14381  xblss2  14382  metcnpi3  14494  limcimolemlt  14610  limccnp2cntop  14623  dvmulxxbr  14643  dvcoapbr  14648  2lgsoddprmlem1  14931  2sqlem8a  14947  2sqlem8  14948