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

Theorem syl21anc 1210
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 531 . 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  4704  brcogw  4995  funprg  5455  funtpg  5456  fnunsn  5506  fresaun  5570  fvun1  5750  iinpreima  5821  ftpg  5879  fsnunf  5903  soisores  6005  isotr  6014  off  6323  caofrss  6342  caonncan  6347  oaf1o  6990  omeulem1  7009  oeordi  7014  oelimcl  7027  oeeulem  7028  oeeui  7029  oaabs2  7072  omabs  7074  pmresg  7228  ralxpmap  7250  domunsncan  7399  mapunen  7468  sucdom2  7495  unxpdom2  7509  sucxpdom  7510  ac6sfi  7544  unblem4  7555  fodomfi  7578  hartogslem1  7744  brwdom2  7776  cantnflt  7868  cantnflem3  7887  cantnflem4  7888  cantnfltOLD  7898  cantnflem3OLD  7909  cantnflem4OLD  7910  cnfcomlem  7920  cnfcom  7921  cnfcomlemOLD  7928  cnfcomOLD  7929  infxpenlem  8168  infxpenc  8172  infxpencOLD  8177  fseqenlem1  8182  pwsdompw  8361  cfeq0  8413  cofsmo  8426  cfsmolem  8427  ssfin4  8467  hsmexlem4  8586  hsmexlem5  8587  axdc3lem2  8608  axdc3lem4  8610  fpwwe2  8798  wunpr  8864  mulclpi  9050  mulcanenq  9117  distrlem4pr  9183  prlem934  9190  prlem936  9204  divge0d  11051  fseq1p1m1  11518  elfznelfzob  11615  seqcaopr2  11826  facavg  12061  hashimarn  12184  swrdspsleq  12326  cats1un  12354  f1oun2prg  12511  sqrdiv  12739  sqrdivd  12894  mulcn2  13057  o1of2  13074  fsumsplit  13200  sumsplit  13219  isumless  13291  demoivreALT  13468  rpnnen2lem11  13490  qredeu  13776  isprm5  13781  rpexp  13789  rpdvds  13793  divnumden  13809  divdenle  13810  phimullem  13837  pythagtriplem4  13869  pythagtriplem8  13873  pythagtriplem9  13874  pcgcd1  13926  sumhash  13941  fldivp1  13942  pockthlem  13949  ssc2  14718  mndpropd  15429  grpidssd  15582  grpinvssd  15583  issubg2  15676  isnsg3  15695  eqgid  15713  gass  15799  symgextres  15910  gsmsymgreqlem2  15916  sylow1lem5  16081  sylow2alem2  16097  sylow3lem3  16108  efgredlemd  16221  efgredlem  16224  frgpnabllem1  16331  frgpnabllem2  16332  subgdmdprd  16505  ablfacrplem  16540  issrngd  16870  lmodprop2d  16931  lsspropd  17020  pwssplit1  17062  lspvadd  17099  mplsubglem  17444  mplsubglemOLD  17446  mplind  17516  znidomb  17836  znrrg  17840  lindfind  18087  lindsind  18088  mdetunilem1  18260  mdetunilem3  18262  mdetunilem4  18263  mdetunilem9  18268  cramerimplem2  18332  mretopd  18538  neiptopnei  18578  neitr  18626  ufilen  19345  flimrest  19398  flimclslem  19399  fclsrest  19439  cnextcn  19481  haustsms2  19549  tsmsxplem2  19570  trust  19646  utoptop  19651  restutop  19654  ustuqtop4  19661  utopsnneiplem  19664  utop2nei  19667  utop3cls  19668  isucn2  19696  ucnima  19698  ucncn  19702  fmucnd  19709  trcfilu  19711  comet  19930  metustexhalfOLD  19980  metustexhalf  19981  metustOLD  19984  metust  19985  metustblOLD  19997  metustbl  19998  metutopOLD  19999  psmetutop  20000  nrmmetd  20009  reconnlem1  20245  reconnlem2  20246  fsumcn  20288  cmetcaulem  20641  iscmet3lem1  20644  iscmet3lem2  20645  bcthlem5  20681  rrxdstprj1  20750  minveclem4  20761  ovolfiniun  20826  itg1addlem4  21019  itg1addlem5  21020  itgsplitioo  21157  c1liplem1  21310  dvfsumlem1  21340  plyeq0lem  21563  quotcan  21660  psercnlem1  21775  cxplea  22026  birthdaylem3  22232  musumsum  22417  dvdsmulf1o  22419  dchrelbas4  22467  dchrhash  22495  2sqlem8a  22595  2sqlem8  22596  chto1ub  22610  vmadivsum  22616  dchrisumlem1  22623  dchrvmasumlem2  22632  dchrvmasumiflem1  22635  rpvmasum2  22646  mulog2sumlem2  22669  selberg2lem  22684  pntrmax  22698  pntpbnd1  22720  pntlemb  22731  pntlemj  22737  ercgrg  22850  tglineeltr  22908  colline  22918  miriso  22935  f1otrg  22940  f1otrge  22941  axcontlem9  23041  uhgraun  23068  umgraun  23085  2wlklemA  23276  2wlklemB  23277  2wlklemC  23278  constr3trllem3  23361  vdgrun  23394  vdgrfiun  23395  eupap1  23420  nmblolbii  24022  minvecolem3  24100  minvecolem4  24104  htthlem  24142  bcs2  24407  nmopub2tALT  25136  nmfnleub2  25153  eighmorth  25191  nmophmi  25258  nmopcoadji  25328  hstle  25457  atcvat3i  25623  disjxpin  25754  off2  25783  xppreima2  25789  fgreu  25814  resf1o  25855  fpwrelmap  25858  xrofsup  25878  eliccelico  25890  elicoelioo  25891  iocinif  25894  difioo  25895  ressprs  25939  tleile  25945  toslublem  25951  tosglblem  25953  xrge0addgt0  25977  xrge0adddir  25979  omndmul2  25999  omndmul3  26000  archirng  26029  archirngz  26030  archiabl  26039  gsumle  26098  orngmul  26124  ofldchr  26135  kerf1hrm  26145  metideq  26174  pstmxmet  26178  sqsscirc2  26193  tpr2rico  26196  fmcncfil  26215  lmxrge0  26236  lmdvg  26237  qqhval2lem  26264  qqhf  26269  qqhnm  26273  esumle  26362  gsumesum  26364  esumlef  26367  esumpcvgval  26381  ofcf  26399  imambfm  26531  oddpwdc  26585  eulerpartlems  26591  eulerpartlemb  26599  eulerpartlemt  26602  iwrdsplit  26618  sseqfn  26621  sseqf  26623  sseqfres  26624  ballotlemfc0  26723  ballotlemfcc  26724  ballotlemfrcn0  26760  sgncl  26769  sgnsub  26775  plymulx0  26796  signsplypnf  26799  signsvtn0  26819  signstfvneq0  26821  signsvtp  26832  signsvtn  26833  signlem0  26836  cvxscon  26980  nobndup  27688  nobnddown  27689  mblfinlem3  28274  itg2addnclem3  28289  ftc1cnnclem  28309  neibastop3  28427  mapfzcons  28897  mzpcl34  28912  mzpindd  28927  mzpsubst  28930  diophrw  28942  diophren  28997  irrapxlem1  29008  pellexlem5  29019  acongrep  29168  pwssplit4  29287  phisum  29412  mulltgt0  29589  fnchoice  29596  fmuldfeq  29609  stoweidlem25  29666  stoweidlem34  29675  stoweidlem38  29679  stoweidlem44  29685  stoweidlem48  29689  stoweidlem49  29690  stoweidlem59  29700  stoweidlem60  29701  wallispilem4  29709  stirlinglem5  29719  lincresunit2  30721  bnj927  31464  bnj1536  31549  bnj1001  31653  bnj1280  31713  lautlt  33308  lautcvr  33309  lauteq  33312  lautco  33314  ltrncl  33342  ltrncnvleN  33347  trljat2  33384  cdlemc6  33413  cdleme20c  33528  cdleme20j  33535  cdleme22e  33561  cdleme22eALTN  33562  cdlemg7aN  33842  cdlemg12e  33864  cdlemg17dALTN  33881  cdlemh  34034  cdlemkfid1N  34138  dibglbN  34384  diblss  34388  diclspsn  34412  dih1  34504  dihglbcpreN  34518  dihmeetlem4preN  34524  lcfrlem19  34779
  Copyright terms: Public domain W3C validator