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

Theorem syl21anc 1181
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 520 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
5 syl21anc.4 . 2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
64, 5syl 15 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  wereu2  4390  funprg  5301  fnunsn  5351  fresaun  5412  fvun1  5590  iinpreima  5655  fsnunf  5718  soisores  5824  isotr  5833  off  6093  caofrss  6110  caonncan  6115  oaf1o  6561  omeulem1  6580  oeordi  6585  oelimcl  6598  oeeulem  6599  oeeui  6600  oaabs2  6643  omabs  6645  pmresg  6795  domunsncan  6962  mapunen  7030  sucdom2  7057  unxpdom2  7071  sucxpdom  7072  ac6sfi  7101  unblem4  7112  fodomfi  7135  hartogslem1  7257  brwdom2  7287  cantnflt  7373  cantnflem3  7393  cantnflem4  7394  cnfcomlem  7402  cnfcom  7403  infxpenlem  7641  infxpenc  7645  fseqenlem1  7651  pwsdompw  7830  cfeq0  7882  cofsmo  7895  cfsmolem  7896  ssfin4  7936  hsmexlem4  8055  hsmexlem5  8056  axdc3lem2  8077  axdc3lem4  8079  fpwwe2  8265  wunpr  8331  mulclpi  8517  mulcanenq  8584  distrlem4pr  8650  prlem934  8657  prlem936  8671  divge0d  10426  fseq1p1m1  10857  seqcaopr2  11082  facavg  11314  cats1un  11476  sqrdiv  11751  sqrdivd  11906  mulcn2  12069  o1of2  12086  fsumsplit  12212  sumsplit  12231  isumless  12304  demoivreALT  12481  rpnnen2lem11  12503  qredeu  12786  isprm5  12791  rpexp  12799  rpdvds  12803  divnumden  12819  divdenle  12820  phimullem  12847  pythagtriplem4  12872  pythagtriplem8  12876  pythagtriplem9  12877  pcgcd1  12929  sumhash  12944  fldivp1  12945  pockthlem  12952  ssc2  13699  mndpropd  14398  issubg2  14636  isnsg3  14651  eqgid  14669  gass  14755  sylow1lem5  14913  sylow2alem2  14929  sylow3lem3  14940  efgredlemd  15053  efgredlem  15056  frgpnabllem1  15161  frgpnabllem2  15162  subgdmdprd  15269  ablfacrplem  15300  issrngd  15626  lmodprop2d  15687  lsspropd  15774  lspvadd  15849  mplsubglem  16179  mplind  16243  znidomb  16515  znrrg  16519  mretopd  16829  ufilen  17625  flimrest  17678  flimclslem  17679  fclsrest  17719  haustsms2  17819  tsmsxplem2  17836  comet  18059  nrmmetd  18097  reconnlem1  18331  reconnlem2  18332  fsumcn  18374  cmetcaulem  18714  iscmet3lem1  18717  iscmet3lem2  18718  bcthlem5  18750  bcth2  18752  minveclem4  18796  ovolfiniun  18860  itg1addlem4  19054  itg1addlem5  19055  itgsplitioo  19192  c1liplem1  19343  dvfsumlem1  19373  plyeq0lem  19592  quotcan  19689  psercnlem1  19801  cxplea  20043  birthdaylem3  20248  musumsum  20432  dvdsmulf1o  20434  dchrelbas4  20482  dchrhash  20510  2sqlem8a  20610  2sqlem8  20611  chto1ub  20625  vmadivsum  20631  dchrisumlem1  20638  dchrvmasumlem2  20647  dchrvmasumiflem1  20650  rpvmasum2  20661  mulog2sumlem2  20684  selberg2lem  20699  pntrmax  20713  pntpbnd1  20735  pntlemb  20746  pntlemj  20752  nmblolbii  21377  minvecolem3  21455  minvecolem4  21459  htthlem  21497  bcs2  21761  nmopub2tALT  22489  nmfnleub2  22506  eighmorth  22544  nmophmi  22611  nmopcoadji  22681  hstle  22810  atcvat3i  22976  ballotlemsgt1  23069  ballotlemfrcn0  23088  cvxscon  23185  umgraun  23290  vdgrun  23304  eupap1  23311  nobndup  23765  nobnddown  23766  axcontlem9  24011  clscnc  25422  isig2a2  25478  neibastop3  25723  ralxpmap  26173  mapfzcons  26205  mzpcl34  26221  mzpindd  26236  mzpsubst  26238  diophrw  26250  diophren  26308  irrapxlem1  26319  pellexlem5  26330  acongrep  26479  pwssplit1  26600  pwssplit4  26603  lindfind  26698  lindsind  26699  phisum  26930  f1oun2prg  27487  uslgraun  27519  bnj927  28173  bnj1536  28259  bnj1001  28363  bnj1280  28423  lautlt  29653  lautcvr  29654  lauteq  29657  lautco  29659  ltrncl  29687  ltrncnvleN  29692  trljat2  29729  cdlemc6  29758  cdleme20c  29873  cdleme20j  29880  cdleme22e  29906  cdleme22eALTN  29907  cdlemg7aN  30187  cdlemg12e  30209  cdlemg17dALTN  30226  cdlemh  30379  cdlemkfid1N  30483  dibglbN  30729  diblss  30733  diclspsn  30757  dih1  30849  dihglbcpreN  30863  dihmeetlem4preN  30869  lcfrlem19  31124
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 177  df-an 360
  Copyright terms: Public domain W3C validator