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  7227  enq0tr  7765  ltmul12a  9151  lt2msq1  9176  ledivp1  9194  lemul1ad  9230  lemul2ad  9231  lediv2ad  10070  xaddge0  10230  difelfznle  10491  expubnd  10982  nn0leexp2  11097  expcanlem  11102  expcand  11104  hashmap  11217  swrds1  11385  ccatswrd  11387  pfxfv  11401  swrdccatin1  11442  pfxccatin12lem3  11449  xrmaxaddlem  11970  mertenslemi1  12246  eftlub  12401  dvdsadd  12547  3dvds  12575  divalgmod  12638  bitsfzolem  12665  bitsfzo  12666  bitsmod  12667  bitsinv1lem  12672  gcdzeq  12743  rplpwr  12748  sqgcd  12750  bezoutr  12753  rpmulgcd2  12817  rpdvds  12821  isprm5  12864  divgcdodd  12865  oddpwdclemxy  12891  divnumden  12918  crth  12946  phimullem  12947  coprimeprodsq2  12981  pythagtriplem19  13005  pclemub  13010  pcpre1  13015  pcidlem  13046  pockthlem  13079  prmunb  13085  kerf1ghm  14027  elrhmunit  14422  rrgnz  14515  znunit  14933  xblss2ps  15395  xblss2  15396  metcnpi3  15508  limcimolemlt  15655  limccnp2cntop  15668  dvmulxxbr  15693  dvcoapbr  15698  ltexp2d  15933  pellexlem3  15973  mpodvdsmulf1o  15984  lgsquad2lem2  16081  2lgsoddprmlem1  16104  2sqlem8a  16121  2sqlem8  16122