Theorem syl21anc 1273

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  4445  brcogw  4929  funprg  5411  funtpg  5412  fnunsn  5470  fun2d  5543  ftpg  5873  fsnunf  5889  isotr  5995  off  6288  caofrss  6307  suppssfvg  6476  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  pmresg  6923  ac6sfi  7168  tridc  7170  eqsndc  7176  tpfidceq  7203  fidcenumlemrks  7236  sbthlemi8  7247  casefun  7389  caseinj  7393  djufun  7408  djuinj  7410  mulclpi  7659  archnqq  7748  addlocprlemlt  7862  addlocprlemeq  7864  addlocprlemgt  7865  mullocprlem  7901  apreim  8894  subrecap  9130  ltrec1  9179  divge0d  10088  fseq1p1m1  10450  q2submod  10771  seq3caopr2  10879  seqcaopr2g  10880  seq3distr  10918  facavg  11133  swrdwrdsymbg  11381  cats1un  11438  shftfibg  11530  sqrtdiv  11752  sqrtdivd  11878  mulcn2  12022  demoivreALT  12485  dvdslegcd  12685  gcdnncl  12688  qredeu  12819  rpdvds  12821  rpexp  12875  oddpwdclemodd  12894  divnumden  12918  divdenle  12919  phimullem  12947  phisum  12963  pythagtriplem4  12991  pythagtriplem8  12995  pythagtriplem9  12996  pcgcd1  13051  fldivp1  13071  pockthlem  13079  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemfrcn0  13217  setsfun  13331  setsfun0  13332  strleund  13400  ercpbl  13595  sgrppropd  13676  mndpropd  13701  grpidssd  13831  grpinvssd  13832  issubg2m  13942  isnsg3  13960  eqgid  13979  kerf1ghm  14027  lmodprop2d  14622  lsspropdg  14705  znidomb  14932  znrrg  14934  comet  15490  fsumcncntop  15558  mulcncf  15599  mpodvdsmulf1o  15984  gausslemma2dlem0d  16051  gausslemma2dlem1a  16057  2lgslem1a1  16085  2sqlem8a  16121  2sqlem8  16122  trilpo  16953  neapmkv  16980