Theorem syl31anc 1172

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 1118	. 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 403	1 |- ( ph -> et )

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  syl32anc  1177  stoic4b  1362  enq0tr  6624  ltmul12a  7938  lt2msq1  7963  ledivp1  7981  lemul1ad  8017  lemul2ad  8018  lediv2ad  8796  difelfznle  9146  expubnd  9533  expcanlem  9643  expcand  9645  dvdsadd  10238  divalgmod  10327  gcdzeq  10411  rplpwr  10416  sqgcd  10418  bezoutr  10421  rpmulgcd2  10477  rpdvds  10481  divgcdodd  10522  oddpwdclemxy  10547