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  5838  fsnunf  5854  isotr  5957  off  6248  caofrss  6267  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  pmresg  6845  ac6sfi  7087  tridc  7089  eqsndc  7095  tpfidceq  7122  fidcenumlemrks  7152  sbthlemi8  7163  casefun  7284  caseinj  7288  djufun  7303  djuinj  7305  mulclpi  7548  archnqq  7637  addlocprlemlt  7751  addlocprlemeq  7753  addlocprlemgt  7754  mullocprlem  7790  apreim  8783  subrecap  9019  ltrec1  9068  divge0d  9972  fseq1p1m1  10329  q2submod  10648  seq3caopr2  10756  seqcaopr2g  10757  seq3distr  10795  facavg  11009  swrdwrdsymbg  11249  cats1un  11306  shftfibg  11398  sqrtdiv  11620  sqrtdivd  11746  mulcn2  11890  demoivreALT  12353  dvdslegcd  12553  gcdnncl  12556  qredeu  12687  rpdvds  12689  rpexp  12743  oddpwdclemodd  12762  divnumden  12786  divdenle  12787  phimullem  12815  phisum  12831  pythagtriplem4  12859  pythagtriplem8  12863  pythagtriplem9  12864  pcgcd1  12919  fldivp1  12939  pockthlem  12947  setsfun  13135  setsfun0  13136  strleund  13204  ercpbl  13432  sgrppropd  13514  mndpropd  13541  grpidssd  13677  grpinvssd  13678  issubg2m  13794  isnsg3  13812  eqgid  13831  kerf1ghm  13879  lmodprop2d  14381  lsspropdg  14464  znidomb  14691  znrrg  14693  comet  15242  fsumcncntop  15310  mulcncf  15351  mpodvdsmulf1o  15733  gausslemma2dlem0d  15800  gausslemma2dlem1a  15806  2lgslem1a1  15834  2sqlem8a  15870  2sqlem8  15871  trilpo  16698  neapmkv  16724