Theorem syl121anc 1243

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 306	. 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 1238	1 |- ( ph -> et )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  syl122anc  1247  tfisi  4587  tfrcllemsucfn  6354  sbthlemi6  6961  sbthlemi8  6963  div32apd  8771  div13apd  8772  expdivapd  10668  modfsummodlemstep  11465  pcqmul  12303  pcid  12323  pcneg  12324  pc2dvds  12329  pcz  12331  pcaddlem  12338  pcadd  12339  pcmpt2  12342  pcbc  12349  qexpz  12350  expnprm  12351  ennnfonelemg  12404  ssblex  13934