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  4734  tfrcllemsucfn  6624  sbthlemi6  7279  sbthlemi8  7281  div32apd  9144  div13apd  9145  expdivapd  11125  swrdsbslen  11438  modfsummodlemstep  12224  pcqmul  13082  pcid  13103  pcneg  13104  pc2dvds  13109  pcz  13111  pcaddlem  13118  pcadd  13119  pcmpt2  13123  pcbc  13130  qexpz  13131  expnprm  13132  ennnfonelemg  13294  ssblex  15532  depind  16750