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  7653  ltmul12a  9039  lt2msq1  9064  ledivp1  9082  lemul1ad  9118  lemul2ad  9119  lediv2ad  9953  xaddge0  10112  difelfznle  10369  expubnd  10857  nn0leexp2  10971  expcanlem  10976  expcand  10978  swrds1  11248  ccatswrd  11250  pfxfv  11264  swrdccatin1  11305  pfxccatin12lem3  11312  xrmaxaddlem  11820  mertenslemi1  12095  eftlub  12250  dvdsadd  12396  3dvds  12424  divalgmod  12487  bitsfzolem  12514  bitsfzo  12515  bitsmod  12516  bitsinv1lem  12521  gcdzeq  12592  rplpwr  12597  sqgcd  12599  bezoutr  12602  rpmulgcd2  12666  rpdvds  12670  isprm5  12713  divgcdodd  12714  oddpwdclemxy  12740  divnumden  12767  crth  12795  phimullem  12796  coprimeprodsq2  12830  pythagtriplem19  12854  pclemub  12859  pcpre1  12864  pcidlem  12895  pockthlem  12928  prmunb  12934  kerf1ghm  13860  elrhmunit  14190  rrgnz  14281  znunit  14672  xblss2ps  15127  xblss2  15128  metcnpi3  15240  limcimolemlt  15387  limccnp2cntop  15400  dvmulxxbr  15425  dvcoapbr  15430  ltexp2d  15665  mpodvdsmulf1o  15713  lgsquad2lem2  15810  2lgsoddprmlem1  15833  2sqlem8a  15850  2sqlem8  15851