Theorem syl21anc 1272

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  4416  brcogw  4899  funprg  5380  funtpg  5381  fnunsn  5439  fun2d  5510  ftpg  5837  fsnunf  5853  isotr  5956  off  6247  caofrss  6266  tfr1onlembxssdm  6508  tfrcllembxssdm  6521  pmresg  6844  ac6sfi  7086  tridc  7088  eqsndc  7094  tpfidceq  7121  fidcenumlemrks  7151  sbthlemi8  7162  casefun  7283  caseinj  7287  djufun  7302  djuinj  7304  mulclpi  7547  archnqq  7636  addlocprlemlt  7750  addlocprlemeq  7752  addlocprlemgt  7753  mullocprlem  7789  apreim  8782  subrecap  9018  ltrec1  9067  divge0d  9971  fseq1p1m1  10328  q2submod  10646  seq3caopr2  10754  seqcaopr2g  10755  seq3distr  10793  facavg  11007  swrdwrdsymbg  11244  cats1un  11301  shftfibg  11380  sqrtdiv  11602  sqrtdivd  11728  mulcn2  11872  demoivreALT  12334  dvdslegcd  12534  gcdnncl  12537  qredeu  12668  rpdvds  12670  rpexp  12724  oddpwdclemodd  12743  divnumden  12767  divdenle  12768  phimullem  12796  phisum  12812  pythagtriplem4  12840  pythagtriplem8  12844  pythagtriplem9  12845  pcgcd1  12900  fldivp1  12920  pockthlem  12928  setsfun  13116  setsfun0  13117  strleund  13185  ercpbl  13413  sgrppropd  13495  mndpropd  13522  grpidssd  13658  grpinvssd  13659  issubg2m  13775  isnsg3  13793  eqgid  13812  kerf1ghm  13860  lmodprop2d  14361  lsspropdg  14444  znidomb  14671  znrrg  14673  comet  15222  fsumcncntop  15290  mulcncf  15331  mpodvdsmulf1o  15713  gausslemma2dlem0d  15780  gausslemma2dlem1a  15786  2lgslem1a1  15814  2sqlem8a  15850  2sqlem8  15851  trilpo  16647  neapmkv  16672