Theorem syl31anc 1276

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 1203	. 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 1004

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 1006

This theorem is referenced by:  syl32anc  1281  stoic4b  1477  enq0tr  7654  ltmul12a  9040  lt2msq1  9065  ledivp1  9083  lemul1ad  9119  lemul2ad  9120  lediv2ad  9954  xaddge0  10113  difelfznle  10370  expubnd  10859  nn0leexp2  10973  expcanlem  10978  expcand  10980  swrds1  11253  ccatswrd  11255  pfxfv  11269  swrdccatin1  11310  pfxccatin12lem3  11317  xrmaxaddlem  11838  mertenslemi1  12114  eftlub  12269  dvdsadd  12415  3dvds  12443  divalgmod  12506  bitsfzolem  12533  bitsfzo  12534  bitsmod  12535  bitsinv1lem  12540  gcdzeq  12611  rplpwr  12616  sqgcd  12618  bezoutr  12621  rpmulgcd2  12685  rpdvds  12689  isprm5  12732  divgcdodd  12733  oddpwdclemxy  12759  divnumden  12786  crth  12814  phimullem  12815  coprimeprodsq2  12849  pythagtriplem19  12873  pclemub  12878  pcpre1  12883  pcidlem  12914  pockthlem  12947  prmunb  12953  kerf1ghm  13879  elrhmunit  14210  rrgnz  14301  znunit  14692  xblss2ps  15147  xblss2  15148  metcnpi3  15260  limcimolemlt  15407  limccnp2cntop  15420  dvmulxxbr  15445  dvcoapbr  15450  ltexp2d  15685  mpodvdsmulf1o  15733  lgsquad2lem2  15830  2lgsoddprmlem1  15853  2sqlem8a  15870  2sqlem8  15871