Theorem syl21anc 1237

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 309	. 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 104

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

This theorem is referenced by:  issod  4319  brcogw  4796  funprg  5266  funtpg  5267  fnunsn  5323  ftpg  5700  fsnunf  5716  isotr  5816  off  6094  caofrss  6106  tfr1onlembxssdm  6343  tfrcllembxssdm  6356  pmresg  6675  ac6sfi  6897  tridc  6898  fidcenumlemrks  6951  sbthlemi8  6962  casefun  7083  caseinj  7087  djufun  7102  djuinj  7104  mulclpi  7326  archnqq  7415  addlocprlemlt  7529  addlocprlemeq  7531  addlocprlemgt  7532  mullocprlem  7568  apreim  8559  subrecap  8795  ltrec1  8844  divge0d  9736  fseq1p1m1  10093  q2submod  10384  seq3caopr2  10481  seq3distr  10512  facavg  10725  shftfibg  10828  sqrtdiv  11050  sqrtdivd  11176  mulcn2  11319  demoivreALT  11780  dvdslegcd  11964  gcdnncl  11967  qredeu  12096  rpdvds  12098  rpexp  12152  oddpwdclemodd  12171  divnumden  12195  divdenle  12196  phimullem  12224  phisum  12239  pythagtriplem4  12267  pythagtriplem8  12271  pythagtriplem9  12272  pcgcd1  12326  fldivp1  12345  pockthlem  12353  setsfun  12496  setsfun0  12497  strleund  12561  ercpbl  12749  mndpropd  12840  grpidssd  12945  grpinvssd  12946  issubg2m  13047  isnsg3  13065  eqgid  13083  comet  13935  fsumcncntop  13992  mulcncf  14027  2sqlem8a  14405  2sqlem8  14406  trilpo  14727  neapmkv  14751