Theorem syl21anc 1248

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  4355  brcogw  4836  funprg  5309  funtpg  5310  fnunsn  5368  ftpg  5749  fsnunf  5765  isotr  5866  off  6152  caofrss  6171  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  pmresg  6744  ac6sfi  6968  tridc  6969  tpfidceq  7000  fidcenumlemrks  7028  sbthlemi8  7039  casefun  7160  caseinj  7164  djufun  7179  djuinj  7181  mulclpi  7412  archnqq  7501  addlocprlemlt  7615  addlocprlemeq  7617  addlocprlemgt  7618  mullocprlem  7654  apreim  8647  subrecap  8883  ltrec1  8932  divge0d  9829  fseq1p1m1  10186  q2submod  10494  seq3caopr2  10602  seqcaopr2g  10603  seq3distr  10641  facavg  10855  shftfibg  11002  sqrtdiv  11224  sqrtdivd  11350  mulcn2  11494  demoivreALT  11956  dvdslegcd  12156  gcdnncl  12159  qredeu  12290  rpdvds  12292  rpexp  12346  oddpwdclemodd  12365  divnumden  12389  divdenle  12390  phimullem  12418  phisum  12434  pythagtriplem4  12462  pythagtriplem8  12466  pythagtriplem9  12467  pcgcd1  12522  fldivp1  12542  pockthlem  12550  setsfun  12738  setsfun0  12739  strleund  12806  ercpbl  13033  sgrppropd  13115  mndpropd  13142  grpidssd  13278  grpinvssd  13279  issubg2m  13395  isnsg3  13413  eqgid  13432  kerf1ghm  13480  lmodprop2d  13980  lsspropdg  14063  znidomb  14290  znrrg  14292  comet  14819  fsumcncntop  14887  mulcncf  14928  mpodvdsmulf1o  15310  gausslemma2dlem0d  15377  gausslemma2dlem1a  15383  2lgslem1a1  15411  2sqlem8a  15447  2sqlem8  15448  trilpo  15774  neapmkv  15799