Theorem syl31anc 1175

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 1121	. 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 922

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 924

This theorem is referenced by:  syl32anc  1180  stoic4b  1365  enq0tr  6914  ltmul12a  8233  lt2msq1  8258  ledivp1  8276  lemul1ad  8312  lemul2ad  8313  lediv2ad  9105  difelfznle  9451  expubnd  9863  expcanlem  9973  expcand  9975  dvdsadd  10633  divalgmod  10721  gcdzeq  10805  rplpwr  10810  sqgcd  10812  bezoutr  10815  rpmulgcd2  10871  rpdvds  10875  divgcdodd  10916  oddpwdclemxy  10941  divnumden  10968  crth  10994  phimullem  10995