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

Theorem syl21anc 1226
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  4862  brcogw  5157  funprg  5623  funtpg  5624  fnunsn  5674  fresaun  5742  fvun1  5925  iinpreima  5998  ftpg  6062  fsnunf  6090  soisores  6204  isotr  6213  off  6535  caofrss  6554  caonncan  6559  fvmpt2curryd  6998  oaf1o  7210  omeulem1  7229  oeordi  7234  oelimcl  7247  oeeulem  7248  oeeui  7249  oaabs2  7292  omabs  7294  pmresg  7444  ralxpmap  7466  domunsncan  7615  mapunen  7684  sucdom2  7712  unxpdom2  7726  sucxpdom  7727  ac6sfi  7762  unblem4  7773  fodomfi  7797  hartogslem1  7965  brwdom2  7997  cantnflt  8089  cantnflem3  8108  cantnflem4  8109  cantnfltOLD  8119  cantnflem3OLD  8130  cantnflem4OLD  8131  cnfcomlem  8141  cnfcom  8142  cnfcomlemOLD  8149  cnfcomOLD  8150  infxpenlem  8389  infxpenc  8393  infxpencOLD  8398  fseqenlem1  8403  pwsdompw  8582  cfeq0  8634  cofsmo  8647  cfsmolem  8648  ssfin4  8688  hsmexlem4  8807  hsmexlem5  8808  axdc3lem2  8829  axdc3lem4  8831  fpwwe2  9019  wunpr  9085  mulclpi  9269  mulcanenq  9336  distrlem4pr  9402  prlem934  9409  prlem936  9423  divge0d  11296  fseq1p1m1  11756  elfznelfzob  11890  seqcaopr2  12117  facavg  12353  hashimarn  12470  swrdspsleq  12647  cats1un  12675  f1oun2prg  12839  sqrtdiv  13073  sqrtdivd  13229  mulcn2  13392  o1of2  13409  fsumsplit  13536  sumsplit  13557  isumless  13631  demoivreALT  13808  rpnnen2lem11  13830  qredeu  14120  isprm5  14125  rpexp  14133  rpdvds  14137  divnumden  14153  divdenle  14154  phimullem  14181  pythagtriplem4  14215  pythagtriplem8  14219  pythagtriplem9  14220  pcgcd1  14272  sumhash  14287  fldivp1  14288  pockthlem  14295  ssc2  15063  mndpropd  15815  grpidssd  15983  grpinvssd  15984  issubg2  16085  isnsg3  16104  eqgid  16122  gass  16208  symgextres  16319  gsmsymgreqlem2  16325  sylow1lem5  16491  sylow2alem2  16507  sylow3lem3  16518  efgredlemd  16631  efgredlem  16634  frgpnabllem1  16746  frgpnabllem2  16747  subgdmdprd  16949  ablfacrplem  16984  kerf1hrm  17260  issrngd  17378  lmodprop2d  17440  lsspropd  17531  pwssplit1  17573  lspvadd  17610  mplsubglem  17961  mplsubglemOLD  17963  mplind  18035  znidomb  18467  znrrg  18471  lindfind  18718  lindsind  18719  mat1ghm  18852  mdetunilem1  18981  mdetunilem3  18983  mdetunilem4  18984  mdetunilem9  18989  cramerimplem2  19053  mat2pmatlin  19103  monmatcollpw  19147  cpmadugsumlemF  19244  mretopd  19459  neiptopnei  19499  neitr  19547  ufilen  20297  flimrest  20350  flimclslem  20351  fclsrest  20391  cnextcn  20433  haustsms2  20501  tsmsxplem2  20522  trust  20598  utoptop  20603  restutop  20606  ustuqtop4  20613  utopsnneiplem  20616  utop2nei  20619  utop3cls  20620  isucn2  20648  ucnima  20650  ucncn  20654  fmucnd  20661  trcfilu  20663  comet  20882  metustexhalfOLD  20932  metustexhalf  20933  metustOLD  20936  metust  20937  metustblOLD  20949  metustbl  20950  metutopOLD  20951  psmetutop  20952  nrmmetd  20961  reconnlem1  21197  reconnlem2  21198  fsumcn  21240  cmetcaulem  21593  iscmet3lem1  21596  iscmet3lem2  21597  bcthlem5  21633  rrxdstprj1  21702  minveclem4  21713  ovolfiniun  21778  itg1addlem4  21972  itg1addlem5  21973  itgsplitioo  22110  c1liplem1  22263  dvfsumlem1  22293  plyeq0lem  22473  quotcan  22570  psercnlem1  22685  cxplea  22942  birthdaylem3  23148  musumsum  23333  dvdsmulf1o  23335  dchrelbas4  23383  dchrhash  23411  2sqlem8a  23511  2sqlem8  23512  chto1ub  23526  vmadivsum  23532  dchrisumlem1  23539  dchrvmasumlem2  23548  dchrvmasumiflem1  23551  rpvmasum2  23562  mulog2sumlem2  23585  selberg2lem  23600  pntrmax  23614  pntpbnd1  23636  pntlemb  23647  pntlemj  23653  ercgrg  23773  motcgr  23788  tglineeltr  23876  colline  23895  miriso  23915  midexlem  23934  perpneq  23956  foot  23961  f1otrg  24039  f1otrge  24040  axcontlem9  24140  uhgraun  24176  umgraun  24193  2wlklemA  24421  2wlklemB  24422  2wlklemC  24423  constr3trllem3  24517  vdgrun  24766  vdgrfiun  24767  eupap1  24841  nmblolbii  25579  minvecolem3  25657  minvecolem4  25661  htthlem  25699  bcs2  25964  nmopub2tALT  26693  nmfnleub2  26710  eighmorth  26748  nmophmi  26815  nmopcoadji  26885  hstle  27014  atcvat3i  27180  disjxpin  27312  off2  27346  xppreima2  27353  fgreu  27378  resf1o  27418  fpwrelmap  27421  xrofsup  27447  eliccelico  27453  elicoelioo  27454  iocinif  27457  difioo  27458  gcdnncl  27472  2sqcoprm  27501  2sqmod  27502  ressprs  27509  tleile  27515  xrge0addgt0  27547  xrge0adddir  27548  omndmul3  27569  archirng  27598  archirngz  27599  gsumle  27636  orngmul  27659  qtophaus  27705  locfinref  27710  metideq  27738  sqsscirc2  27757  tpr2rico  27760  fmcncfil  27779  lmxrge0  27800  lmdvg  27801  qqhval2lem  27828  qqhf  27833  qqhnm  27837  esumle  27931  gsumesum  27933  esumlef  27936  esumpcvgval  27950  ofcf  27968  imambfm  28099  oddpwdc  28159  eulerpartlems  28165  eulerpartlemb  28173  eulerpartlemt  28176  iwrdsplit  28192  sseqfn  28195  sseqf  28197  sseqfres  28198  ballotlemfc0  28297  ballotlemfcc  28298  ballotlemfrcn0  28334  sgnsub  28349  plymulx0  28370  signsplypnf  28373  signsvtn0  28393  signstfvneq0  28395  signsvtp  28406  signsvtn  28407  cvxscon  28554  elmrsubrn  28746  nobndup  29428  nobnddown  29429  mblfinlem3  30021  itg2addnclem3  30036  ftc1cnnclem  30056  neibastop3  30148  mapfzcons  30616  mzpcl34  30631  mzpindd  30646  mzpsubst  30649  diophrw  30660  diophren  30715  irrapxlem1  30726  pellexlem5  30737  acongrep  30886  pwssplit4  31003  phisum  31128  mulltgt0  31344  fnchoice  31351  3adantlr3  31364  3adantll2  31368  3adantll3  31369  fmuldfeq  31501  limccog  31530  limcrecl  31539  lptioo1  31542  islpcn  31549  limsupre  31551  neglimc  31557  0ellimcdiv  31559  limclner  31561  icccncfext  31593  stoweidlem25  31692  stoweidlem34  31701  stoweidlem38  31705  stoweidlem44  31711  stoweidlem48  31715  stoweidlem49  31716  stoweidlem59  31726  stoweidlem60  31727  wallispilem4  31735  stirlinglem5  31745  dirkercncflem2  31771  fourierdlem39  31813  fourierdlem42  31816  fourierdlem46  31820  fourierdlem47  31821  fourierdlem48  31822  fourierdlem50  31824  fourierdlem51  31825  fourierdlem64  31838  fourierdlem73  31847  fourierdlem74  31848  fourierdlem77  31851  fourierdlem80  31854  fourierdlem87  31861  fourierdlem94  31868  fourierdlem103  31877  fourierdlem104  31878  uhgun  32214  estrreslem1  32481  lincresunit2  32789  4an4132  32976  bnj927  33534  bnj1536  33619  bnj1001  33723  bnj1280  33783  lautlt  35517  lautcvr  35518  lauteq  35521  lautco  35523  ltrncl  35551  ltrncnvleN  35556  trljat2  35594  cdlemc6  35623  cdleme20c  35739  cdleme20j  35746  cdleme22e  35772  cdleme22eALTN  35773  cdlemg7aN  36053  cdlemg12e  36075  cdlemg17dALTN  36092  cdlemh  36245  cdlemkfid1N  36349  dibglbN  36595  diblss  36599  diclspsn  36623  dih1  36715  dihglbcpreN  36729  dihmeetlem4preN  36735  lcfrlem19  36990
  Copyright terms: Public domain W3C validator