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  7617  ltmul12a  9003  lt2msq1  9028  ledivp1  9046  lemul1ad  9082  lemul2ad  9083  lediv2ad  9911  xaddge0  10070  difelfznle  10327  expubnd  10813  nn0leexp2  10927  expcanlem  10932  expcand  10934  swrds1  11195  ccatswrd  11197  pfxfv  11211  swrdccatin1  11252  pfxccatin12lem3  11259  xrmaxaddlem  11766  mertenslemi1  12041  eftlub  12196  dvdsadd  12342  3dvds  12370  divalgmod  12433  bitsfzolem  12460  bitsfzo  12461  bitsmod  12462  bitsinv1lem  12467  gcdzeq  12538  rplpwr  12543  sqgcd  12545  bezoutr  12548  rpmulgcd2  12612  rpdvds  12616  isprm5  12659  divgcdodd  12660  oddpwdclemxy  12686  divnumden  12713  crth  12741  phimullem  12742  coprimeprodsq2  12776  pythagtriplem19  12800  pclemub  12805  pcpre1  12810  pcidlem  12841  pockthlem  12874  prmunb  12880  kerf1ghm  13806  elrhmunit  14135  rrgnz  14226  znunit  14617  xblss2ps  15072  xblss2  15073  metcnpi3  15185  limcimolemlt  15332  limccnp2cntop  15345  dvmulxxbr  15370  dvcoapbr  15375  ltexp2d  15610  mpodvdsmulf1o  15658  lgsquad2lem2  15755  2lgsoddprmlem1  15778  2sqlem8a  15795  2sqlem8  15796