Theorem syl31anc 1252

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 1179	. 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 980

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 982

This theorem is referenced by:  syl32anc  1257  stoic4b  1444  enq0tr  7496  ltmul12a  8881  lt2msq1  8906  ledivp1  8924  lemul1ad  8960  lemul2ad  8961  lediv2ad  9788  xaddge0  9947  difelfznle  10204  expubnd  10670  nn0leexp2  10784  expcanlem  10789  expcand  10791  xrmaxaddlem  11406  mertenslemi1  11681  eftlub  11836  dvdsadd  11982  divalgmod  12071  gcdzeq  12162  rplpwr  12167  sqgcd  12169  bezoutr  12172  rpmulgcd2  12236  rpdvds  12240  isprm5  12283  divgcdodd  12284  oddpwdclemxy  12310  divnumden  12337  crth  12365  phimullem  12366  coprimeprodsq2  12399  pythagtriplem19  12423  pclemub  12428  pcpre1  12433  pcidlem  12464  pockthlem  12497  prmunb  12503  kerf1ghm  13347  elrhmunit  13676  rrgnz  13767  znunit  14158  xblss2ps  14583  xblss2  14584  metcnpi3  14696  limcimolemlt  14843  limccnp2cntop  14856  dvmulxxbr  14881  dvcoapbr  14886  lgsquad2lem2  15239  2lgsoddprmlem1  15262  2sqlem8a  15279  2sqlem8  15280