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

Theorem syl21anc 1217
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 534 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
5 syl21anc.4 . 2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
64, 5syl 16 1  |-  ( ph  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  wereu2  4738  brcogw  5029  funprg  5488  funtpg  5489  fnunsn  5539  fresaun  5603  fvun1  5783  iinpreima  5854  ftpg  5913  fsnunf  5937  soisores  6039  isotr  6048  off  6355  caofrss  6374  caonncan  6379  fvmpt2curryd  6811  oaf1o  7023  omeulem1  7042  oeordi  7047  oelimcl  7060  oeeulem  7061  oeeui  7062  oaabs2  7105  omabs  7107  pmresg  7261  ralxpmap  7283  domunsncan  7432  mapunen  7501  sucdom2  7528  unxpdom2  7542  sucxpdom  7543  ac6sfi  7577  unblem4  7588  fodomfi  7611  hartogslem1  7777  brwdom2  7809  cantnflt  7901  cantnflem3  7920  cantnflem4  7921  cantnfltOLD  7931  cantnflem3OLD  7942  cantnflem4OLD  7943  cnfcomlem  7953  cnfcom  7954  cnfcomlemOLD  7961  cnfcomOLD  7962  infxpenlem  8201  infxpenc  8205  infxpencOLD  8210  fseqenlem1  8215  pwsdompw  8394  cfeq0  8446  cofsmo  8459  cfsmolem  8460  ssfin4  8500  hsmexlem4  8619  hsmexlem5  8620  axdc3lem2  8641  axdc3lem4  8643  fpwwe2  8831  wunpr  8897  mulclpi  9083  mulcanenq  9150  distrlem4pr  9216  prlem934  9223  prlem936  9237  divge0d  11084  fseq1p1m1  11555  elfznelfzob  11652  seqcaopr2  11863  facavg  12098  hashimarn  12221  swrdspsleq  12363  cats1un  12391  f1oun2prg  12548  sqrdiv  12776  sqrdivd  12931  mulcn2  13094  o1of2  13111  fsumsplit  13237  sumsplit  13256  isumless  13329  demoivreALT  13506  rpnnen2lem11  13528  qredeu  13814  isprm5  13819  rpexp  13827  rpdvds  13831  divnumden  13847  divdenle  13848  phimullem  13875  pythagtriplem4  13907  pythagtriplem8  13911  pythagtriplem9  13912  pcgcd1  13964  sumhash  13979  fldivp1  13980  pockthlem  13987  ssc2  14756  mndpropd  15467  grpidssd  15623  grpinvssd  15624  issubg2  15717  isnsg3  15736  eqgid  15754  gass  15840  symgextres  15951  gsmsymgreqlem2  15957  sylow1lem5  16122  sylow2alem2  16138  sylow3lem3  16149  efgredlemd  16262  efgredlem  16265  frgpnabllem1  16372  frgpnabllem2  16373  subgdmdprd  16553  ablfacrplem  16588  kerf1hrm  16853  issrngd  16968  lmodprop2d  17029  lsspropd  17120  pwssplit1  17162  lspvadd  17199  mplsubglem  17532  mplsubglemOLD  17534  mplind  17606  znidomb  18016  znrrg  18020  lindfind  18267  lindsind  18268  mdetunilem1  18440  mdetunilem3  18442  mdetunilem4  18443  mdetunilem9  18448  cramerimplem2  18512  mretopd  18718  neiptopnei  18758  neitr  18806  ufilen  19525  flimrest  19578  flimclslem  19579  fclsrest  19619  cnextcn  19661  haustsms2  19729  tsmsxplem2  19750  trust  19826  utoptop  19831  restutop  19834  ustuqtop4  19841  utopsnneiplem  19844  utop2nei  19847  utop3cls  19848  isucn2  19876  ucnima  19878  ucncn  19882  fmucnd  19889  trcfilu  19891  comet  20110  metustexhalfOLD  20160  metustexhalf  20161  metustOLD  20164  metust  20165  metustblOLD  20177  metustbl  20178  metutopOLD  20179  psmetutop  20180  nrmmetd  20189  reconnlem1  20425  reconnlem2  20426  fsumcn  20468  cmetcaulem  20821  iscmet3lem1  20824  iscmet3lem2  20825  bcthlem5  20861  rrxdstprj1  20930  minveclem4  20941  ovolfiniun  21006  itg1addlem4  21199  itg1addlem5  21200  itgsplitioo  21337  c1liplem1  21490  dvfsumlem1  21520  plyeq0lem  21700  quotcan  21797  psercnlem1  21912  cxplea  22163  birthdaylem3  22369  musumsum  22554  dvdsmulf1o  22556  dchrelbas4  22604  dchrhash  22632  2sqlem8a  22732  2sqlem8  22733  chto1ub  22747  vmadivsum  22753  dchrisumlem1  22760  dchrvmasumlem2  22769  dchrvmasumiflem1  22772  rpvmasum2  22783  mulog2sumlem2  22806  selberg2lem  22821  pntrmax  22835  pntpbnd1  22857  pntlemb  22868  pntlemj  22874  ercgrg  22991  tglineeltr  23059  colline  23074  miriso  23095  midexlem  23108  perpneq  23127  foot  23132  f1otrg  23139  f1otrge  23140  axcontlem9  23240  uhgraun  23267  umgraun  23284  2wlklemA  23475  2wlklemB  23476  2wlklemC  23477  constr3trllem3  23560  vdgrun  23593  vdgrfiun  23594  eupap1  23619  nmblolbii  24221  minvecolem3  24299  minvecolem4  24303  htthlem  24341  bcs2  24606  nmopub2tALT  25335  nmfnleub2  25352  eighmorth  25390  nmophmi  25457  nmopcoadji  25527  hstle  25656  atcvat3i  25822  disjxpin  25952  off2  25981  xppreima2  25987  fgreu  26012  resf1o  26052  fpwrelmap  26055  xrofsup  26077  eliccelico  26089  elicoelioo  26090  iocinif  26093  difioo  26094  ressprs  26138  tleile  26144  toslublem  26150  tosglblem  26152  xrge0addgt0  26176  xrge0adddir  26177  omndmul2  26197  omndmul3  26198  archirng  26227  archirngz  26228  archiabl  26237  gsumle  26268  orngmul  26293  ofldchr  26304  metideq  26342  pstmxmet  26346  sqsscirc2  26361  tpr2rico  26364  fmcncfil  26383  lmxrge0  26404  lmdvg  26405  qqhval2lem  26432  qqhf  26437  qqhnm  26441  esumle  26530  gsumesum  26532  esumlef  26535  esumpcvgval  26549  ofcf  26567  imambfm  26699  oddpwdc  26759  eulerpartlems  26765  eulerpartlemb  26773  eulerpartlemt  26776  iwrdsplit  26792  sseqfn  26795  sseqf  26797  sseqfres  26798  ballotlemfc0  26897  ballotlemfcc  26898  ballotlemfrcn0  26934  sgncl  26943  sgnsub  26949  plymulx0  26970  signsplypnf  26973  signsvtn0  26993  signstfvneq0  26995  signsvtp  27006  signsvtn  27007  signlem0  27010  cvxscon  27154  nobndup  27863  nobnddown  27864  mblfinlem3  28456  itg2addnclem3  28471  ftc1cnnclem  28491  neibastop3  28609  mapfzcons  29078  mzpcl34  29093  mzpindd  29108  mzpsubst  29111  diophrw  29123  diophren  29178  irrapxlem1  29189  pellexlem5  29200  acongrep  29349  pwssplit4  29468  phisum  29593  mulltgt0  29770  fnchoice  29777  fmuldfeq  29790  stoweidlem25  29846  stoweidlem34  29855  stoweidlem38  29859  stoweidlem44  29865  stoweidlem48  29869  stoweidlem49  29870  stoweidlem59  29880  stoweidlem60  29881  wallispilem4  29889  stirlinglem5  29899  lincresunit2  31009  bnj927  31858  bnj1536  31943  bnj1001  32047  bnj1280  32107  lautlt  33831  lautcvr  33832  lauteq  33835  lautco  33837  ltrncl  33865  ltrncnvleN  33870  trljat2  33907  cdlemc6  33936  cdleme20c  34051  cdleme20j  34058  cdleme22e  34084  cdleme22eALTN  34085  cdlemg7aN  34365  cdlemg12e  34387  cdlemg17dALTN  34404  cdlemh  34557  cdlemkfid1N  34661  dibglbN  34907  diblss  34911  diclspsn  34935  dih1  35027  dihglbcpreN  35041  dihmeetlem4preN  35047  lcfrlem19  35302
  Copyright terms: Public domain W3C validator