Theorem syl121anc 1283

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl122anc  1287  tfisi  4736  tfrcllemsucfn  6628  sbthlemi6  7284  sbthlemi8  7286  div32apd  9152  div13apd  9153  expdivapd  11146  swrdsbslen  11460  modfsummodlemstep  12249  pcqmul  13111  pcid  13132  pcneg  13133  pc2dvds  13138  pcz  13140  pcaddlem  13147  pcadd  13148  pcmpt2  13152  pcbc  13159  qexpz  13160  expnprm  13161  ennnfonelemg  13352  ssblex  15657  bcmono  16304  depind  16955