Theorem syl31anc 1274

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 1201	. 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 1002

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 1004

This theorem is referenced by:  syl32anc  1279  stoic4b  1475  enq0tr  7644  ltmul12a  9030  lt2msq1  9055  ledivp1  9073  lemul1ad  9109  lemul2ad  9110  lediv2ad  9944  xaddge0  10103  difelfznle  10360  expubnd  10848  nn0leexp2  10962  expcanlem  10967  expcand  10969  swrds1  11239  ccatswrd  11241  pfxfv  11255  swrdccatin1  11296  pfxccatin12lem3  11303  xrmaxaddlem  11811  mertenslemi1  12086  eftlub  12241  dvdsadd  12387  3dvds  12415  divalgmod  12478  bitsfzolem  12505  bitsfzo  12506  bitsmod  12507  bitsinv1lem  12512  gcdzeq  12583  rplpwr  12588  sqgcd  12590  bezoutr  12593  rpmulgcd2  12657  rpdvds  12661  isprm5  12704  divgcdodd  12705  oddpwdclemxy  12731  divnumden  12758  crth  12786  phimullem  12787  coprimeprodsq2  12821  pythagtriplem19  12845  pclemub  12850  pcpre1  12855  pcidlem  12886  pockthlem  12919  prmunb  12925  kerf1ghm  13851  elrhmunit  14181  rrgnz  14272  znunit  14663  xblss2ps  15118  xblss2  15119  metcnpi3  15231  limcimolemlt  15378  limccnp2cntop  15391  dvmulxxbr  15416  dvcoapbr  15421  ltexp2d  15656  mpodvdsmulf1o  15704  lgsquad2lem2  15801  2lgsoddprmlem1  15824  2sqlem8a  15841  2sqlem8  15842