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  7267  enq0tr  7807  ltmul12a  9198  lt2msq1  9223  ledivp1  9241  lemul1ad  9277  lemul2ad  9278  lediv2ad  10136  xaddge0  10296  difelfznle  10558  expubnd  11053  nn0leexp2  11169  expcanlem  11174  expcand  11176  hashmap  11289  swrds1  11461  ccatswrd  11463  pfxfv  11477  swrdccatin1  11518  pfxccatin12lem3  11525  xrmaxaddlem  12050  mertenslemi1  12326  eftlub  12481  dvdsadd  12627  3dvds  12655  divalgmod  12718  bitsfzolem  12745  bitsfzo  12746  bitsmod  12747  bitsinv1lem  12752  gcdzeq  12823  rplpwr  12828  sqgcd  12830  bezoutr  12833  rpmulgcd2  12897  rpdvds  12901  isprm5  12945  divgcdodd  12946  nnmaxpwlemxy  12972  divnumden  13000  crth  13030  phimullem  13031  coprimeprodsq2  13065  pythagtriplem19  13089  pclemub  13094  pcpre1  13099  pcidlem  13130  pockthlem  13163  prmunb  13169  kerf1ghm  14135  elrhmunit  14592  rrgnz  14685  znunit  15102  xblss2ps  15647  xblss2  15648  metcnpi3  15760  limcimolemlt  15907  limccnp2cntop  15920  dvmulxxbr  15945  dvcoapbr  15950  ltexp2d  16195  pellexlem3  16248  mpodvdsmulf1o  16301  bposlem1  16328  lgsquad2lem2  16423  2lgsoddprmlem1  16446  2sqlem8a  16463  2sqlem8  16464