Theorem syl31anc 1277

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 1204	. 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 1005

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 1007

This theorem is referenced by:  syl32anc  1282  stoic4b  1478  enq0tr  7697  ltmul12a  9083  lt2msq1  9108  ledivp1  9126  lemul1ad  9162  lemul2ad  9163  lediv2ad  9997  xaddge0  10156  difelfznle  10413  expubnd  10902  nn0leexp2  11016  expcanlem  11021  expcand  11023  swrds1  11296  ccatswrd  11298  pfxfv  11312  swrdccatin1  11353  pfxccatin12lem3  11360  xrmaxaddlem  11881  mertenslemi1  12157  eftlub  12312  dvdsadd  12458  3dvds  12486  divalgmod  12549  bitsfzolem  12576  bitsfzo  12577  bitsmod  12578  bitsinv1lem  12583  gcdzeq  12654  rplpwr  12659  sqgcd  12661  bezoutr  12664  rpmulgcd2  12728  rpdvds  12732  isprm5  12775  divgcdodd  12776  oddpwdclemxy  12802  divnumden  12829  crth  12857  phimullem  12858  coprimeprodsq2  12892  pythagtriplem19  12916  pclemub  12921  pcpre1  12926  pcidlem  12957  pockthlem  12990  prmunb  12996  kerf1ghm  13922  elrhmunit  14253  rrgnz  14344  znunit  14735  xblss2ps  15195  xblss2  15196  metcnpi3  15308  limcimolemlt  15455  limccnp2cntop  15468  dvmulxxbr  15493  dvcoapbr  15498  ltexp2d  15733  mpodvdsmulf1o  15781  lgsquad2lem2  15878  2lgsoddprmlem1  15901  2sqlem8a  15918  2sqlem8  15919