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  7265  enq0tr  7807  ltmul12a  9198  lt2msq1  9223  ledivp1  9241  lemul1ad  9277  lemul2ad  9278  lediv2ad  10137  xaddge0  10297  difelfznle  10559  expubnd  11054  nn0leexp2  11170  expcanlem  11175  expcand  11177  hashmap  11290  swrds1  11462  ccatswrd  11464  pfxfv  11478  swrdccatin1  11519  pfxccatin12lem3  11526  xrmaxaddlem  12051  mertenslemi1  12327  eftlub  12482  dvdsadd  12628  3dvds  12656  divalgmod  12719  bitsfzolem  12746  bitsfzo  12747  bitsmod  12748  bitsinv1lem  12753  gcdzeq  12824  rplpwr  12829  sqgcd  12831  bezoutr  12834  rpmulgcd2  12898  rpdvds  12902  isprm5  12946  divgcdodd  12947  nnmaxpwlemxy  12973  divnumden  13001  crth  13031  phimullem  13032  coprimeprodsq2  13066  pythagtriplem19  13090  pclemub  13095  pcpre1  13100  pcidlem  13131  pockthlem  13164  prmunb  13170  kerf1ghm  14136  elrhmunit  14593  rrgnz  14686  znunit  15103  xblss2ps  15630  xblss2  15631  metcnpi3  15743  limcimolemlt  15890  limccnp2cntop  15903  dvmulxxbr  15928  dvcoapbr  15933  ltexp2d  16178  pellexlem3  16231  mpodvdsmulf1o  16284  bposlem1  16311  lgsquad2lem2  16406  2lgsoddprmlem1  16429  2sqlem8a  16446  2sqlem8  16447