Theorem syl121anc 1238

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 1233	1 |- ( ph -> et )

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

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 975

This theorem is referenced by:  syl122anc  1242  tfisi  4571  tfrcllemsucfn  6332  sbthlemi6  6939  sbthlemi8  6941  div32apd  8731  div13apd  8732  expdivapd  10623  modfsummodlemstep  11420  pcqmul  12257  pcid  12277  pcneg  12278  pc2dvds  12283  pcz  12285  pcaddlem  12292  pcadd  12293  pcmpt2  12296  pcbc  12303  qexpz  12304  expnprm  12305  ennnfonelemg  12358  ssblex  13225