Theorem syl121anc 1233

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 )
syl121anc.5	|- ( ( ps /\ ( ch /\ th ) /\ ta ) -> et )

Assertion

Ref	Expression
syl121anc	|- ( ph -> et )

Proof of Theorem syl121anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. 2 |- ( ph -> ps )
2		sylXanc.2	. . 3 |- ( ph -> ch )
3		sylXanc.3	. . 3 |- ( ph -> th )
4	2, 3	jca 304	. 2 |- ( ph -> ( ch /\ th ) )
5		sylXanc.4	. 2 |- ( ph -> ta )
6		syl121anc.5	. 2 |- ( ( ps /\ ( ch /\ th ) /\ ta ) -> et )
7	1, 4, 5, 6	syl3anc 1228	1 |- ( ph -> et )

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

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 970

This theorem is referenced by:  syl122anc  1237  tfisi  4563  tfrcllemsucfn  6317  sbthlemi6  6923  sbthlemi8  6925  div32apd  8706  div13apd  8707  expdivapd  10598  modfsummodlemstep  11394  pcqmul  12231  pcid  12251  pcneg  12252  pc2dvds  12257  pcz  12259  pcaddlem  12266  pcadd  12267  pcmpt2  12270  pcbc  12277  qexpz  12278  expnprm  12279  ennnfonelemg  12332  ssblex  13031