Theorem syl21anc 1227

Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)

Hypotheses

Ref	Expression
sylXanc.1	|- ( ph -> ps )
sylXanc.2	|- ( ph -> ch )
sylXanc.3	|- ( ph -> th )
syl21anc.4	|- ( ( ( ps /\ ch ) /\ th ) -> ta )

Assertion

Ref	Expression
syl21anc	|- ( ph -> ta )

Proof of Theorem syl21anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 |- ( ph -> ps )
2		sylXanc.2	. . 3 |- ( ph -> ch )
3		sylXanc.3	. . 3 |- ( ph -> th )
4	1, 2, 3	jca31 307	. 2 |- ( ph -> ( ( ps /\ ch ) /\ th ) )
5		syl21anc.4	. 2 |- ( ( ( ps /\ ch ) /\ th ) -> ta )
6	4, 5	syl 14	1 |- ( ph -> ta )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  issod  4297  brcogw  4773  funprg  5238  funtpg  5239  fnunsn  5295  ftpg  5669  fsnunf  5685  isotr  5784  off  6062  caofrss  6074  tfr1onlembxssdm  6311  tfrcllembxssdm  6324  pmresg  6642  ac6sfi  6864  tridc  6865  fidcenumlemrks  6918  sbthlemi8  6929  casefun  7050  caseinj  7054  djufun  7069  djuinj  7071  mulclpi  7269  archnqq  7358  addlocprlemlt  7472  addlocprlemeq  7474  addlocprlemgt  7475  mullocprlem  7511  apreim  8501  subrecap  8735  ltrec1  8783  divge0d  9673  fseq1p1m1  10029  q2submod  10320  seq3caopr2  10417  seq3distr  10448  facavg  10659  shftfibg  10762  sqrtdiv  10984  sqrtdivd  11110  mulcn2  11253  demoivreALT  11714  dvdslegcd  11897  gcdnncl  11900  qredeu  12029  rpdvds  12031  rpexp  12085  oddpwdclemodd  12104  divnumden  12128  divdenle  12129  phimullem  12157  phisum  12172  pythagtriplem4  12200  pythagtriplem8  12204  pythagtriplem9  12205  pcgcd1  12259  fldivp1  12278  pockthlem  12286  setsfun  12429  setsfun0  12430  strleund  12483  comet  13149  fsumcncntop  13206  mulcncf  13241  2sqlem8a  13608  2sqlem8  13609  trilpo  13932  neapmkv  13956