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  4321  brcogw  4798  funprg  5268  funtpg  5269  fnunsn  5325  ftpg  5702  fsnunf  5718  isotr  5819  off  6097  caofrss  6109  tfr1onlembxssdm  6346  tfrcllembxssdm  6359  pmresg  6678  ac6sfi  6900  tridc  6901  fidcenumlemrks  6954  sbthlemi8  6965  casefun  7086  caseinj  7090  djufun  7105  djuinj  7107  mulclpi  7329  archnqq  7418  addlocprlemlt  7532  addlocprlemeq  7534  addlocprlemgt  7535  mullocprlem  7571  apreim  8562  subrecap  8798  ltrec1  8847  divge0d  9739  fseq1p1m1  10096  q2submod  10387  seq3caopr2  10484  seq3distr  10515  facavg  10728  shftfibg  10831  sqrtdiv  11053  sqrtdivd  11179  mulcn2  11322  demoivreALT  11783  dvdslegcd  11967  gcdnncl  11970  qredeu  12099  rpdvds  12101  rpexp  12155  oddpwdclemodd  12174  divnumden  12198  divdenle  12199  phimullem  12227  phisum  12242  pythagtriplem4  12270  pythagtriplem8  12274  pythagtriplem9  12275  pcgcd1  12329  fldivp1  12348  pockthlem  12356  setsfun  12499  setsfun0  12500  strleund  12564  ercpbl  12755  mndpropd  12846  grpidssd  12951  grpinvssd  12952  issubg2m  13054  isnsg3  13072  eqgid  13090  lmodprop2d  13443  comet  14038  fsumcncntop  14095  mulcncf  14130  2sqlem8a  14508  2sqlem8  14509  trilpo  14830  neapmkv  14855