Theorem syl31anc 1219

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 1161	. 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 408	1 |- ( ph -> et )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  syl32anc  1224  stoic4b  1409  enq0tr  7242  ltmul12a  8618  lt2msq1  8643  ledivp1  8661  lemul1ad  8697  lemul2ad  8698  lediv2ad  9506  xaddge0  9661  difelfznle  9912  expubnd  10350  expcanlem  10462  expcand  10464  xrmaxaddlem  11029  mertenslemi1  11304  eftlub  11396  dvdsadd  11536  divalgmod  11624  gcdzeq  11710  rplpwr  11715  sqgcd  11717  bezoutr  11720  rpmulgcd2  11776  rpdvds  11780  divgcdodd  11821  oddpwdclemxy  11847  divnumden  11874  crth  11900  phimullem  11901  xblss2ps  12573  xblss2  12574  metcnpi3  12686  limcimolemlt  12802  limccnp2cntop  12815  dvmulxxbr  12835  dvcoapbr  12840