Theorem syl31anc 1241

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 1177	. 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 978

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 980

This theorem is referenced by:  syl32anc  1246  stoic4b  1433  enq0tr  7432  ltmul12a  8816  lt2msq1  8841  ledivp1  8859  lemul1ad  8895  lemul2ad  8896  lediv2ad  9718  xaddge0  9877  difelfznle  10134  expubnd  10576  nn0leexp2  10689  expcanlem  10694  expcand  10696  xrmaxaddlem  11267  mertenslemi1  11542  eftlub  11697  dvdsadd  11842  divalgmod  11931  gcdzeq  12022  rplpwr  12027  sqgcd  12029  bezoutr  12032  rpmulgcd2  12094  rpdvds  12098  isprm5  12141  divgcdodd  12142  oddpwdclemxy  12168  divnumden  12195  crth  12223  phimullem  12224  coprimeprodsq2  12257  pythagtriplem19  12281  pclemub  12286  pcpre1  12291  pcidlem  12321  pockthlem  12353  prmunb  12359  xblss2ps  13874  xblss2  13875  metcnpi3  13987  limcimolemlt  14103  limccnp2cntop  14116  dvmulxxbr  14136  dvcoapbr  14141  2lgsoddprmlem1  14423  2sqlem8a  14439  2sqlem8  14440