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  1452  enq0tr  7546  ltmul12a  8932  lt2msq1  8957  ledivp1  8975  lemul1ad  9011  lemul2ad  9012  lediv2ad  9840  xaddge0  9999  difelfznle  10256  expubnd  10739  nn0leexp2  10853  expcanlem  10858  expcand  10860  xrmaxaddlem  11542  mertenslemi1  11817  eftlub  11972  dvdsadd  12118  3dvds  12146  divalgmod  12209  bitsfzolem  12236  bitsfzo  12237  bitsmod  12238  bitsinv1lem  12243  gcdzeq  12314  rplpwr  12319  sqgcd  12321  bezoutr  12324  rpmulgcd2  12388  rpdvds  12392  isprm5  12435  divgcdodd  12436  oddpwdclemxy  12462  divnumden  12489  crth  12517  phimullem  12518  coprimeprodsq2  12552  pythagtriplem19  12576  pclemub  12581  pcpre1  12586  pcidlem  12617  pockthlem  12650  prmunb  12656  kerf1ghm  13581  elrhmunit  13910  rrgnz  14001  znunit  14392  xblss2ps  14847  xblss2  14848  metcnpi3  14960  limcimolemlt  15107  limccnp2cntop  15120  dvmulxxbr  15145  dvcoapbr  15150  ltexp2d  15385  mpodvdsmulf1o  15433  lgsquad2lem2  15530  2lgsoddprmlem1  15553  2sqlem8a  15570  2sqlem8  15571