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  mapfi  7214  enq0tr  7749  ltmul12a  9134  lt2msq1  9159  ledivp1  9177  lemul1ad  9213  lemul2ad  9214  lediv2ad  10052  xaddge0  10211  difelfznle  10469  expubnd  10958  nn0leexp2  11072  expcanlem  11077  expcand  11079  hashmap  11192  swrds1  11360  ccatswrd  11362  pfxfv  11376  swrdccatin1  11417  pfxccatin12lem3  11424  xrmaxaddlem  11945  mertenslemi1  12221  eftlub  12376  dvdsadd  12522  3dvds  12550  divalgmod  12613  bitsfzolem  12640  bitsfzo  12641  bitsmod  12642  bitsinv1lem  12647  gcdzeq  12718  rplpwr  12723  sqgcd  12725  bezoutr  12728  rpmulgcd2  12792  rpdvds  12796  isprm5  12839  divgcdodd  12840  oddpwdclemxy  12866  divnumden  12893  crth  12921  phimullem  12922  coprimeprodsq2  12956  pythagtriplem19  12980  pclemub  12985  pcpre1  12990  pcidlem  13021  pockthlem  13054  prmunb  13060  kerf1ghm  13991  elrhmunit  14322  rrgnz  14414  znunit  14807  xblss2ps  15269  xblss2  15270  metcnpi3  15382  limcimolemlt  15529  limccnp2cntop  15542  dvmulxxbr  15567  dvcoapbr  15572  ltexp2d  15807  pellexlem3  15847  mpodvdsmulf1o  15858  lgsquad2lem2  15955  2lgsoddprmlem1  15978  2sqlem8a  15995  2sqlem8  15996