Theorem syl31anc 1230

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 1166	. 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 409	1 |- ( ph -> et )

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

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 969

This theorem is referenced by:  syl32anc  1235  stoic4b  1420  enq0tr  7366  ltmul12a  8746  lt2msq1  8771  ledivp1  8789  lemul1ad  8825  lemul2ad  8826  lediv2ad  9646  xaddge0  9805  difelfznle  10060  expubnd  10502  nn0leexp2  10613  expcanlem  10617  expcand  10619  xrmaxaddlem  11187  mertenslemi1  11462  eftlub  11617  dvdsadd  11761  divalgmod  11849  gcdzeq  11940  rplpwr  11945  sqgcd  11947  bezoutr  11950  rpmulgcd2  12006  rpdvds  12010  divgcdodd  12052  oddpwdclemxy  12078  divnumden  12105  crth  12133  phimullem  12134  coprimeprodsq2  12167  pythagtriplem19  12191  pclemub  12196  pcpre1  12201  pcidlem  12231  xblss2ps  12945  xblss2  12946  metcnpi3  13058  limcimolemlt  13174  limccnp2cntop  13187  dvmulxxbr  13207  dvcoapbr  13212