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  7501  ltmul12a  8887  lt2msq1  8912  ledivp1  8930  lemul1ad  8966  lemul2ad  8967  lediv2ad  9794  xaddge0  9953  difelfznle  10210  expubnd  10688  nn0leexp2  10802  expcanlem  10807  expcand  10809  xrmaxaddlem  11425  mertenslemi1  11700  eftlub  11855  dvdsadd  12001  3dvds  12029  divalgmod  12092  bitsfzolem  12118  bitsfzo  12119  gcdzeq  12189  rplpwr  12194  sqgcd  12196  bezoutr  12199  rpmulgcd2  12263  rpdvds  12267  isprm5  12310  divgcdodd  12311  oddpwdclemxy  12337  divnumden  12364  crth  12392  phimullem  12393  coprimeprodsq2  12427  pythagtriplem19  12451  pclemub  12456  pcpre1  12461  pcidlem  12492  pockthlem  12525  prmunb  12531  kerf1ghm  13404  elrhmunit  13733  rrgnz  13824  znunit  14215  xblss2ps  14640  xblss2  14641  metcnpi3  14753  limcimolemlt  14900  limccnp2cntop  14913  dvmulxxbr  14938  dvcoapbr  14943  ltexp2d  15178  mpodvdsmulf1o  15226  lgsquad2lem2  15323  2lgsoddprmlem1  15346  2sqlem8a  15363  2sqlem8  15364