MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl21anc Unicode version

Theorem syl21anc 1183
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
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
41, 2, 3jca31 521 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
5 syl21anc.4 . 2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
64, 5syl 16 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  wereu2  4521  brcogw  4982  funprg  5441  funtpg  5442  fnunsn  5493  fresaun  5555  fvun1  5734  iinpreima  5800  ftpg  5856  fsnunf  5871  soisores  5987  isotr  5996  off  6260  caofrss  6277  caonncan  6282  oaf1o  6743  omeulem1  6762  oeordi  6767  oelimcl  6780  oeeulem  6781  oeeui  6782  oaabs2  6825  omabs  6827  pmresg  6978  domunsncan  7145  mapunen  7213  sucdom2  7240  unxpdom2  7254  sucxpdom  7255  ac6sfi  7288  unblem4  7299  fodomfi  7322  hartogslem1  7445  brwdom2  7475  cantnflt  7561  cantnflem3  7581  cantnflem4  7582  cnfcomlem  7590  cnfcom  7591  infxpenlem  7829  infxpenc  7833  fseqenlem1  7839  pwsdompw  8018  cfeq0  8070  cofsmo  8083  cfsmolem  8084  ssfin4  8124  hsmexlem4  8243  hsmexlem5  8244  axdc3lem2  8265  axdc3lem4  8267  fpwwe2  8452  wunpr  8518  mulclpi  8704  mulcanenq  8771  distrlem4pr  8837  prlem934  8844  prlem936  8858  divge0d  10617  fseq1p1m1  11053  elfznelfzob  11121  seqcaopr2  11287  facavg  11520  cats1un  11718  f1oun2prg  11792  sqrdiv  11999  sqrdivd  12154  mulcn2  12317  o1of2  12334  fsumsplit  12461  sumsplit  12480  isumless  12553  demoivreALT  12730  rpnnen2lem11  12752  qredeu  13035  isprm5  13040  rpexp  13048  rpdvds  13052  divnumden  13068  divdenle  13069  phimullem  13096  pythagtriplem4  13121  pythagtriplem8  13125  pythagtriplem9  13126  pcgcd1  13178  sumhash  13193  fldivp1  13194  pockthlem  13201  ssc2  13950  mndpropd  14649  issubg2  14887  isnsg3  14902  eqgid  14920  gass  15006  sylow1lem5  15164  sylow2alem2  15180  sylow3lem3  15191  efgredlemd  15304  efgredlem  15307  frgpnabllem1  15412  frgpnabllem2  15413  subgdmdprd  15520  ablfacrplem  15551  issrngd  15877  lmodprop2d  15934  lsspropd  16021  lspvadd  16096  mplsubglem  16426  mplind  16490  znidomb  16766  znrrg  16770  mretopd  17080  neiptopnei  17120  neitr  17167  ufilen  17884  flimrest  17937  flimclslem  17938  fclsrest  17978  cnextcn  18020  haustsms2  18088  tsmsxplem2  18105  trust  18181  utoptop  18186  restutop  18189  ustuqtop4  18196  utopsnneiplem  18199  utop2nei  18202  utop3cls  18203  isucn2  18231  ucnima  18233  ucncn  18237  fmucnd  18244  trcfilu  18246  comet  18434  metustexhalf  18477  metust  18479  metustbl  18487  metutop  18488  nrmmetd  18494  reconnlem1  18729  reconnlem2  18730  fsumcn  18772  cmetcaulem  19113  iscmet3lem1  19116  iscmet3lem2  19117  bcthlem5  19151  minveclem4  19201  ovolfiniun  19265  itg1addlem4  19459  itg1addlem5  19460  itgsplitioo  19597  c1liplem1  19748  dvfsumlem1  19778  plyeq0lem  19997  quotcan  20094  psercnlem1  20209  cxplea  20455  birthdaylem3  20660  musumsum  20845  dvdsmulf1o  20847  dchrelbas4  20895  dchrhash  20923  2sqlem8a  21023  2sqlem8  21024  chto1ub  21038  vmadivsum  21044  dchrisumlem1  21051  dchrvmasumlem2  21060  dchrvmasumiflem1  21063  rpvmasum2  21074  mulog2sumlem2  21097  selberg2lem  21112  pntrmax  21126  pntpbnd1  21148  pntlemb  21159  pntlemj  21165  uhgraun  21214  umgraun  21231  constr2trl  21447  2pthonlem2  21449  constr3trllem3  21488  vdgrun  21521  vdgrfiun  21522  eupap1  21547  nmblolbii  22149  minvecolem3  22227  minvecolem4  22231  htthlem  22269  bcs2  22533  nmopub2tALT  23261  nmfnleub2  23278  eighmorth  23316  nmophmi  23383  nmopcoadji  23453  hstle  23582  atcvat3i  23748  off2  23898  xppreima2  23903  xrofsup  23963  eliccelico  23977  elicoelioo  23978  iocinif  23981  difioo  23982  xrge0addgt0  24044  xrge0adddir  24045  kerf1hrm  24079  sqsscirc2  24112  tpr2rico  24115  fmcncfil  24122  lmxrge0  24142  lmdvg  24143  qqhval2lem  24165  qqhf  24170  qqhnm  24174  esumle  24246  gsumesum  24248  esumlef  24251  esumpcvgval  24265  ofcf  24283  imambfm  24407  ballotlemfc0  24530  ballotlemfcc  24531  ballotlemfrcn0  24567  cvxscon  24710  nobndup  25379  nobnddown  25380  axcontlem9  25626  ftc1cnnclem  25979  neibastop3  26083  ralxpmap  26434  mapfzcons  26464  mzpcl34  26480  mzpindd  26495  mzpsubst  26497  diophrw  26509  diophren  26566  irrapxlem1  26577  pellexlem5  26588  acongrep  26737  pwssplit1  26858  pwssplit4  26861  lindfind  26956  lindsind  26957  phisum  27188  mulltgt0  27362  fnchoice  27369  fmuldfeq  27382  stoweidlem25  27443  stoweidlem34  27452  stoweidlem38  27456  stoweidlem44  27462  stoweidlem48  27466  stoweidlem49  27467  stoweidlem59  27477  stoweidlem60  27478  wallispilem4  27486  stirlinglem5  27496  bnj927  28478  bnj1536  28564  bnj1001  28668  bnj1280  28728  lautlt  30206  lautcvr  30207  lauteq  30210  lautco  30212  ltrncl  30240  ltrncnvleN  30245  trljat2  30282  cdlemc6  30311  cdleme20c  30426  cdleme20j  30433  cdleme22e  30459  cdleme22eALTN  30460  cdlemg7aN  30740  cdlemg12e  30762  cdlemg17dALTN  30779  cdlemh  30932  cdlemkfid1N  31036  dibglbN  31282  diblss  31286  diclspsn  31310  dih1  31402  dihglbcpreN  31416  dihmeetlem4preN  31422  lcfrlem19  31677
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator