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  4422  brcogw  4905  funprg  5387  funtpg  5388  fnunsn  5446  fun2d  5518  ftpg  5846  fsnunf  5862  isotr  5967  off  6257  caofrss  6276  suppssfvg  6441  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  pmresg  6888  ac6sfi  7130  tridc  7132  eqsndc  7138  tpfidceq  7165  fidcenumlemrks  7195  sbthlemi8  7206  casefun  7327  caseinj  7331  djufun  7346  djuinj  7348  mulclpi  7591  archnqq  7680  addlocprlemlt  7794  addlocprlemeq  7796  addlocprlemgt  7797  mullocprlem  7833  apreim  8825  subrecap  9061  ltrec1  9110  divge0d  10016  fseq1p1m1  10374  q2submod  10693  seq3caopr2  10801  seqcaopr2g  10802  seq3distr  10840  facavg  11054  swrdwrdsymbg  11294  cats1un  11351  shftfibg  11443  sqrtdiv  11665  sqrtdivd  11791  mulcn2  11935  demoivreALT  12398  dvdslegcd  12598  gcdnncl  12601  qredeu  12732  rpdvds  12734  rpexp  12788  oddpwdclemodd  12807  divnumden  12831  divdenle  12832  phimullem  12860  phisum  12876  pythagtriplem4  12904  pythagtriplem8  12908  pythagtriplem9  12909  pcgcd1  12964  fldivp1  12984  pockthlem  12992  setsfun  13180  setsfun0  13181  strleund  13249  ercpbl  13477  sgrppropd  13559  mndpropd  13586  grpidssd  13722  grpinvssd  13723  issubg2m  13839  isnsg3  13857  eqgid  13876  kerf1ghm  13924  lmodprop2d  14427  lsspropdg  14510  znidomb  14737  znrrg  14739  comet  15293  fsumcncntop  15361  mulcncf  15402  mpodvdsmulf1o  15787  gausslemma2dlem0d  15854  gausslemma2dlem1a  15860  2lgslem1a1  15888  2sqlem8a  15924  2sqlem8  15925  trilpo  16758  neapmkv  16784