Theorem syl112anc 1174

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

Assertion

Ref	Expression
syl112anc	|- ( ph -> et )

Proof of Theorem syl112anc

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

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 920

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

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  fvun1  5313  reapmul1  7970  recrecap  8072  rec11rap  8074  divdivdivap  8076  dmdcanap  8085  ddcanap  8089  rerecclap  8093  div2negap  8098  divap1d  8163  divmulapd  8174  divmulap2d  8185  divmulap3d  8186  divassapd  8187  div12apd  8188  div23apd  8189  divdirapd  8190  divsubdirapd  8191  div11apd  8192  ltmul12a  8213  ltdiv1  8221  ltrec  8236  lt2msq1  8238  lediv2  8244  lediv23  8246  recp1lt1  8252  qapne  9017  modqge0  9626  modqlt  9627  modqid  9643  expgt1  9828  nnlesq  9892  expnbnd  9910  facubnd  9986  resqrexlemover  10268  mulcn2  10523  bezoutlemnewy  10763  bezoutlemstep  10764  mulgcd  10783  mulgcddvds  10854  prmind2  10880  oddpwdclemxy  10925  oddpwdclemodd  10928  qnumgt0  10954