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  4440  brcogw  4924  funprg  5406  funtpg  5407  fnunsn  5465  fun2d  5538  ftpg  5868  fsnunf  5884  isotr  5989  off  6279  caofrss  6298  suppssfvg  6463  tfr1onlembxssdm  6574  tfrcllembxssdm  6587  pmresg  6910  ac6sfi  7155  tridc  7157  eqsndc  7163  tpfidceq  7190  fidcenumlemrks  7223  sbthlemi8  7234  casefun  7376  caseinj  7380  djufun  7395  djuinj  7397  mulclpi  7643  archnqq  7732  addlocprlemlt  7846  addlocprlemeq  7848  addlocprlemgt  7849  mullocprlem  7885  apreim  8877  subrecap  9113  ltrec1  9162  divge0d  10070  fseq1p1m1  10428  q2submod  10747  seq3caopr2  10855  seqcaopr2g  10856  seq3distr  10894  facavg  11108  swrdwrdsymbg  11356  cats1un  11413  shftfibg  11505  sqrtdiv  11727  sqrtdivd  11853  mulcn2  11997  demoivreALT  12460  dvdslegcd  12660  gcdnncl  12663  qredeu  12794  rpdvds  12796  rpexp  12850  oddpwdclemodd  12869  divnumden  12893  divdenle  12894  phimullem  12922  phisum  12938  pythagtriplem4  12966  pythagtriplem8  12970  pythagtriplem9  12971  pcgcd1  13026  fldivp1  13046  pockthlem  13054  setsfun  13247  setsfun0  13248  strleund  13316  ercpbl  13544  sgrppropd  13626  mndpropd  13653  grpidssd  13789  grpinvssd  13790  issubg2m  13906  isnsg3  13924  eqgid  13943  kerf1ghm  13991  lmodprop2d  14496  lsspropdg  14579  znidomb  14806  znrrg  14808  comet  15364  fsumcncntop  15432  mulcncf  15473  mpodvdsmulf1o  15858  gausslemma2dlem0d  15925  gausslemma2dlem1a  15931  2lgslem1a1  15959  2sqlem8a  15995  2sqlem8  15996  trilpo  16827  neapmkv  16854