Theorem syl31anc 1281

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 1208	. 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 415	1 |- ( ph -> et )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl32anc  1286  stoic4b  1482  mapfi  7261  enq0tr  7801  ltmul12a  9192  lt2msq1  9217  ledivp1  9235  lemul1ad  9271  lemul2ad  9272  lediv2ad  10130  xaddge0  10290  difelfznle  10552  expubnd  11046  nn0leexp2  11162  expcanlem  11167  expcand  11169  hashmap  11282  swrds1  11454  ccatswrd  11456  pfxfv  11470  swrdccatin1  11511  pfxccatin12lem3  11518  xrmaxaddlem  12042  mertenslemi1  12318  eftlub  12473  dvdsadd  12619  3dvds  12647  divalgmod  12710  bitsfzolem  12737  bitsfzo  12738  bitsmod  12739  bitsinv1lem  12744  gcdzeq  12815  rplpwr  12820  sqgcd  12822  bezoutr  12825  rpmulgcd2  12889  rpdvds  12893  isprm5  12937  divgcdodd  12938  nnmaxpwlemxy  12964  divnumden  12992  crth  13022  phimullem  13023  coprimeprodsq2  13057  pythagtriplem19  13081  pclemub  13086  pcpre1  13091  pcidlem  13122  pockthlem  13155  prmunb  13161  kerf1ghm  14126  elrhmunit  14533  rrgnz  14626  znunit  15043  xblss2ps  15554  xblss2  15555  metcnpi3  15667  limcimolemlt  15814  limccnp2cntop  15827  dvmulxxbr  15852  dvcoapbr  15857  ltexp2d  16097  pellexlem3  16150  mpodvdsmulf1o  16185  bposlem1  16209  lgsquad2lem2  16299  2lgsoddprmlem1  16322  2sqlem8a  16339  2sqlem8  16340