MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl21anc Structured version   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  4571  brcogw  5033  funprg  5492  funtpg  5493  fnunsn  5544  fresaun  5606  fvun1  5786  iinpreima  5852  ftpg  5908  fsnunf  5923  soisores  6039  isotr  6048  off  6312  caofrss  6329  caonncan  6334  oaf1o  6798  omeulem1  6817  oeordi  6822  oelimcl  6835  oeeulem  6836  oeeui  6837  oaabs2  6880  omabs  6882  pmresg  7033  domunsncan  7200  mapunen  7268  sucdom2  7295  unxpdom2  7309  sucxpdom  7310  ac6sfi  7343  unblem4  7354  fodomfi  7377  hartogslem1  7503  brwdom2  7533  cantnflt  7619  cantnflem3  7639  cantnflem4  7640  cnfcomlem  7648  cnfcom  7649  infxpenlem  7887  infxpenc  7891  fseqenlem1  7897  pwsdompw  8076  cfeq0  8128  cofsmo  8141  cfsmolem  8142  ssfin4  8182  hsmexlem4  8301  hsmexlem5  8302  axdc3lem2  8323  axdc3lem4  8325  fpwwe2  8510  wunpr  8576  mulclpi  8762  mulcanenq  8829  distrlem4pr  8895  prlem934  8902  prlem936  8916  divge0d  10676  fseq1p1m1  11114  elfznelfzob  11185  seqcaopr2  11351  facavg  11584  cats1un  11782  f1oun2prg  11856  sqrdiv  12063  sqrdivd  12218  mulcn2  12381  o1of2  12398  fsumsplit  12525  sumsplit  12544  isumless  12617  demoivreALT  12794  rpnnen2lem11  12816  qredeu  13099  isprm5  13104  rpexp  13112  rpdvds  13116  divnumden  13132  divdenle  13133  phimullem  13160  pythagtriplem4  13185  pythagtriplem8  13189  pythagtriplem9  13190  pcgcd1  13242  sumhash  13257  fldivp1  13258  pockthlem  13265  ssc2  14014  mndpropd  14713  issubg2  14951  isnsg3  14966  eqgid  14984  gass  15070  sylow1lem5  15228  sylow2alem2  15244  sylow3lem3  15255  efgredlemd  15368  efgredlem  15371  frgpnabllem1  15476  frgpnabllem2  15477  subgdmdprd  15584  ablfacrplem  15615  issrngd  15941  lmodprop2d  15998  lsspropd  16085  lspvadd  16160  mplsubglem  16490  mplind  16554  znidomb  16834  znrrg  16838  mretopd  17148  neiptopnei  17188  neitr  17236  ufilen  17954  flimrest  18007  flimclslem  18008  fclsrest  18048  cnextcn  18090  haustsms2  18158  tsmsxplem2  18175  trust  18251  utoptop  18256  restutop  18259  ustuqtop4  18266  utopsnneiplem  18269  utop2nei  18272  utop3cls  18273  isucn2  18301  ucnima  18303  ucncn  18307  fmucnd  18314  trcfilu  18316  comet  18535  metustexhalfOLD  18585  metustexhalf  18586  metustOLD  18589  metust  18590  metustblOLD  18602  metustbl  18603  metutopOLD  18604  psmetutop  18605  nrmmetd  18614  reconnlem1  18849  reconnlem2  18850  fsumcn  18892  cmetcaulem  19233  iscmet3lem1  19236  iscmet3lem2  19237  bcthlem5  19273  minveclem4  19325  ovolfiniun  19389  itg1addlem4  19583  itg1addlem5  19584  itgsplitioo  19721  c1liplem1  19872  dvfsumlem1  19902  plyeq0lem  20121  quotcan  20218  psercnlem1  20333  cxplea  20579  birthdaylem3  20784  musumsum  20969  dvdsmulf1o  20971  dchrelbas4  21019  dchrhash  21047  2sqlem8a  21147  2sqlem8  21148  chto1ub  21162  vmadivsum  21168  dchrisumlem1  21175  dchrvmasumlem2  21184  dchrvmasumiflem1  21187  rpvmasum2  21198  mulog2sumlem2  21221  selberg2lem  21236  pntrmax  21250  pntpbnd1  21272  pntlemb  21283  pntlemj  21289  uhgraun  21338  umgraun  21355  2wlklemA  21546  2wlklemB  21547  2wlklemC  21548  constr3trllem3  21631  vdgrun  21664  vdgrfiun  21665  eupap1  21690  nmblolbii  22292  minvecolem3  22370  minvecolem4  22374  htthlem  22412  bcs2  22676  nmopub2tALT  23404  nmfnleub2  23421  eighmorth  23459  nmophmi  23526  nmopcoadji  23596  hstle  23725  atcvat3i  23891  disjxpin  24020  off2  24046  xppreima2  24052  xrofsup  24118  eliccelico  24132  elicoelioo  24133  iocinif  24136  difioo  24137  tleile  24181  toslub  24183  tosglb  24184  xrge0addgt0  24206  xrge0adddir  24207  kerf1hrm  24254  metideq  24280  pstmxmet  24284  sqsscirc2  24299  tpr2rico  24302  fmcncfil  24309  lmxrge0  24329  lmdvg  24330  qqhval2lem  24357  qqhf  24362  qqhnm  24366  esumle  24441  gsumesum  24443  esumlef  24446  esumpcvgval  24460  ofcf  24478  imambfm  24604  sibfof  24646  ballotlemfc0  24742  ballotlemfcc  24743  ballotlemfrcn0  24779  cvxscon  24922  nobndup  25647  nobnddown  25648  axcontlem9  25903  mblfinlem2  26235  itg2addnclem3  26248  ftc1cnnclem  26268  neibastop3  26382  ralxpmap  26733  mapfzcons  26763  mzpcl34  26779  mzpindd  26794  mzpsubst  26796  diophrw  26808  diophren  26865  irrapxlem1  26876  pellexlem5  26887  acongrep  27036  pwssplit1  27156  pwssplit4  27159  lindfind  27254  lindsind  27255  phisum  27486  mulltgt0  27660  fnchoice  27667  fmuldfeq  27680  stoweidlem25  27741  stoweidlem34  27750  stoweidlem38  27754  stoweidlem44  27760  stoweidlem48  27764  stoweidlem49  27765  stoweidlem59  27775  stoweidlem60  27776  wallispilem4  27784  stirlinglem5  27794  hashimarn  28141  bnj927  29076  bnj1536  29162  bnj1001  29266  bnj1280  29326  lautlt  30825  lautcvr  30826  lauteq  30829  lautco  30831  ltrncl  30859  ltrncnvleN  30864  trljat2  30901  cdlemc6  30930  cdleme20c  31045  cdleme20j  31052  cdleme22e  31078  cdleme22eALTN  31079  cdlemg7aN  31359  cdlemg12e  31381  cdlemg17dALTN  31398  cdlemh  31551  cdlemkfid1N  31655  dibglbN  31901  diblss  31905  diclspsn  31929  dih1  32021  dihglbcpreN  32035  dihmeetlem4preN  32041  lcfrlem19  32296
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