MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl21anc 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  4539  brcogw  5000  funprg  5459  funtpg  5460  fnunsn  5511  fresaun  5573  fvun1  5753  iinpreima  5819  ftpg  5875  fsnunf  5890  soisores  6006  isotr  6015  off  6279  caofrss  6296  caonncan  6301  oaf1o  6765  omeulem1  6784  oeordi  6789  oelimcl  6802  oeeulem  6803  oeeui  6804  oaabs2  6847  omabs  6849  pmresg  7000  domunsncan  7167  mapunen  7235  sucdom2  7262  unxpdom2  7276  sucxpdom  7277  ac6sfi  7310  unblem4  7321  fodomfi  7344  hartogslem1  7467  brwdom2  7497  cantnflt  7583  cantnflem3  7603  cantnflem4  7604  cnfcomlem  7612  cnfcom  7613  infxpenlem  7851  infxpenc  7855  fseqenlem1  7861  pwsdompw  8040  cfeq0  8092  cofsmo  8105  cfsmolem  8106  ssfin4  8146  hsmexlem4  8265  hsmexlem5  8266  axdc3lem2  8287  axdc3lem4  8289  fpwwe2  8474  wunpr  8540  mulclpi  8726  mulcanenq  8793  distrlem4pr  8859  prlem934  8866  prlem936  8880  divge0d  10640  fseq1p1m1  11077  elfznelfzob  11148  seqcaopr2  11314  facavg  11547  cats1un  11745  f1oun2prg  11819  sqrdiv  12026  sqrdivd  12181  mulcn2  12344  o1of2  12361  fsumsplit  12488  sumsplit  12507  isumless  12580  demoivreALT  12757  rpnnen2lem11  12779  qredeu  13062  isprm5  13067  rpexp  13075  rpdvds  13079  divnumden  13095  divdenle  13096  phimullem  13123  pythagtriplem4  13148  pythagtriplem8  13152  pythagtriplem9  13153  pcgcd1  13205  sumhash  13220  fldivp1  13221  pockthlem  13228  ssc2  13977  mndpropd  14676  issubg2  14914  isnsg3  14929  eqgid  14947  gass  15033  sylow1lem5  15191  sylow2alem2  15207  sylow3lem3  15218  efgredlemd  15331  efgredlem  15334  frgpnabllem1  15439  frgpnabllem2  15440  subgdmdprd  15547  ablfacrplem  15578  issrngd  15904  lmodprop2d  15961  lsspropd  16048  lspvadd  16123  mplsubglem  16453  mplind  16517  znidomb  16797  znrrg  16801  mretopd  17111  neiptopnei  17151  neitr  17198  ufilen  17915  flimrest  17968  flimclslem  17969  fclsrest  18009  cnextcn  18051  haustsms2  18119  tsmsxplem2  18136  trust  18212  utoptop  18217  restutop  18220  ustuqtop4  18227  utopsnneiplem  18230  utop2nei  18233  utop3cls  18234  isucn2  18262  ucnima  18264  ucncn  18268  fmucnd  18275  trcfilu  18277  comet  18496  metustexhalfOLD  18546  metustexhalf  18547  metustOLD  18550  metust  18551  metustblOLD  18563  metustbl  18564  metutopOLD  18565  psmetutop  18566  nrmmetd  18575  reconnlem1  18810  reconnlem2  18811  fsumcn  18853  cmetcaulem  19194  iscmet3lem1  19197  iscmet3lem2  19198  bcthlem5  19234  minveclem4  19286  ovolfiniun  19350  itg1addlem4  19544  itg1addlem5  19545  itgsplitioo  19682  c1liplem1  19833  dvfsumlem1  19863  plyeq0lem  20082  quotcan  20179  psercnlem1  20294  cxplea  20540  birthdaylem3  20745  musumsum  20930  dvdsmulf1o  20932  dchrelbas4  20980  dchrhash  21008  2sqlem8a  21108  2sqlem8  21109  chto1ub  21123  vmadivsum  21129  dchrisumlem1  21136  dchrvmasumlem2  21145  dchrvmasumiflem1  21148  rpvmasum2  21159  mulog2sumlem2  21182  selberg2lem  21197  pntrmax  21211  pntpbnd1  21233  pntlemb  21244  pntlemj  21250  uhgraun  21299  umgraun  21316  2wlklemA  21507  2wlklemB  21508  2wlklemC  21509  constr3trllem3  21592  vdgrun  21625  vdgrfiun  21626  eupap1  21651  nmblolbii  22253  minvecolem3  22331  minvecolem4  22335  htthlem  22373  bcs2  22637  nmopub2tALT  23365  nmfnleub2  23382  eighmorth  23420  nmophmi  23487  nmopcoadji  23557  hstle  23686  atcvat3i  23852  disjxpin  23981  off2  24007  xppreima2  24013  xrofsup  24079  eliccelico  24093  elicoelioo  24094  iocinif  24097  difioo  24098  tleile  24142  toslub  24144  tosglb  24145  xrge0addgt0  24167  xrge0adddir  24168  kerf1hrm  24215  metideq  24241  pstmxmet  24245  sqsscirc2  24260  tpr2rico  24263  fmcncfil  24270  lmxrge0  24290  lmdvg  24291  qqhval2lem  24318  qqhf  24323  qqhnm  24327  esumle  24402  gsumesum  24404  esumlef  24407  esumpcvgval  24421  ofcf  24439  imambfm  24565  sibfof  24607  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemfrcn0  24740  cvxscon  24883  nobndup  25568  nobnddown  25569  axcontlem9  25815  mblfinlem2  26144  itg2addnclem3  26157  ftc1cnnclem  26177  neibastop3  26281  ralxpmap  26632  mapfzcons  26662  mzpcl34  26678  mzpindd  26693  mzpsubst  26695  diophrw  26707  diophren  26764  irrapxlem1  26775  pellexlem5  26786  acongrep  26935  pwssplit1  27056  pwssplit4  27059  lindfind  27154  lindsind  27155  phisum  27386  mulltgt0  27560  fnchoice  27567  fmuldfeq  27580  stoweidlem25  27641  stoweidlem34  27650  stoweidlem38  27654  stoweidlem44  27660  stoweidlem48  27664  stoweidlem49  27665  stoweidlem59  27675  stoweidlem60  27676  wallispilem4  27684  stirlinglem5  27694  hashimarn  27994  bnj927  28845  bnj1536  28931  bnj1001  29035  bnj1280  29095  lautlt  30573  lautcvr  30574  lauteq  30577  lautco  30579  ltrncl  30607  ltrncnvleN  30612  trljat2  30649  cdlemc6  30678  cdleme20c  30793  cdleme20j  30800  cdleme22e  30826  cdleme22eALTN  30827  cdlemg7aN  31107  cdlemg12e  31129  cdlemg17dALTN  31146  cdlemh  31299  cdlemkfid1N  31403  dibglbN  31649  diblss  31653  diclspsn  31677  dih1  31769  dihglbcpreN  31783  dihmeetlem4preN  31789  lcfrlem19  32044
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