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

Theorem syl21anc 1291
Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
Hypotheses
Ref Expression
syl12anc.1  |-  ( ph  ->  ps )
syl12anc.2  |-  ( ph  ->  ch )
syl12anc.3  |-  ( ph  ->  th )
syl21anc.4  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
Assertion
Ref Expression
syl21anc  |-  ( ph  ->  ta )

Proof of Theorem syl21anc
StepHypRef Expression
1 syl12anc.1 . . 3  |-  ( ph  ->  ps )
2 syl12anc.2 . . 3  |-  ( ph  ->  ch )
3 syl12anc.3 . . 3  |-  ( ph  ->  th )
41, 2, 3jca31 543 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
5 syl21anc.4 . 2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
64, 5syl 17 1  |-  ( ph  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  wereu2  4836  brcogw  5008  funprg  5638  funtpg  5639  funcnvtp  5647  funcnvqp  5648  fnunsn  5693  fresaun  5766  fvun1  5951  iinpreima  6025  ftpg  6090  fsnunf  6118  f1prex  6200  soisores  6236  isotr  6245  off  6565  caofrss  6583  caonncan  6588  fvmpt2curryd  7036  oaf1o  7282  omeulem1  7301  oeordi  7306  oelimcl  7319  oeeulem  7320  oeeui  7321  oaabs2  7364  omabs  7366  pmresg  7517  ralxpmap  7539  domunsncan  7690  mapunen  7759  sucdom2  7786  unxpdom2  7798  sucxpdom  7799  ac6sfi  7833  unblem4  7844  fodomfi  7868  hartogslem1  8075  brwdom2  8106  cantnflt  8195  cantnflem3  8214  cantnflem4  8215  cnfcomlem  8222  cnfcom  8223  infxpenlem  8462  infxpenc  8467  fseqenlem1  8473  pwsdompw  8652  cfeq0  8704  cofsmo  8717  cfsmolem  8718  ssfin4  8758  hsmexlem4  8877  hsmexlem5  8878  axdc3lem2  8899  axdc3lem4  8901  fpwwe2  9086  wunpr  9152  mulclpi  9336  mulcanenq  9403  distrlem4pr  9469  prlem934  9476  prlem936  9490  divge0d  11401  fseq1p1m1  11894  elfznelfzob  12046  seqcaopr2  12287  facavg  12524  hashimarn  12651  cats1un  12886  f1oun2prg  13071  sqrtdiv  13406  sqrtdivd  13562  mulcn2  13736  o1of2  13753  fsumsplit  13883  sumsplit  13906  isumless  13980  demoivreALT  14332  rpnnen2lem11  14354  gcdnncl  14560  isprm5  14730  qredeu  14743  rpexp  14751  rpdvds  14755  divnumden  14776  divdenle  14777  phimullem  14806  pythagtriplem4  14848  pythagtriplem8  14852  pythagtriplem9  14853  pcgcd1  14905  sumhash  14920  fldivp1  14921  pockthlem  14928  ssc2  15805  estrreslem1  16100  mndpropd  16640  grpidssd  16808  grpinvssd  16809  issubg2  16910  isnsg3  16929  eqgid  16947  gass  17033  symgextres  17144  gsmsymgreqlem2  17150  sylow1lem5  17332  sylow2alem2  17348  sylow3lem3  17359  efgredlemd  17472  efgredlem  17475  frgpnabllem1  17587  frgpnabllem2  17588  subgdmdprd  17745  ablfacrplem  17776  kerf1hrm  18049  issrngd  18167  lmodprop2d  18228  lsspropd  18318  pwssplit1  18360  lspvadd  18397  mplsubglem  18735  mplind  18802  znidomb  19209  znrrg  19213  lindfind  19451  lindsind  19452  mat1ghm  19585  mdetunilem1  19714  mdetunilem3  19716  mdetunilem4  19717  mdetunilem9  19722  cramerimplem2  19786  mat2pmatlin  19836  monmatcollpw  19880  cpmadugsumlemF  19977  mretopd  20185  neiptopnei  20225  neitr  20273  ufilen  21023  flimrest  21076  flimclslem  21077  fclsrest  21117  cnextcn  21160  haustsms2  21229  tsmsxplem2  21246  trust  21322  utoptop  21327  restutop  21330  ustuqtop4  21337  utopsnneiplem  21340  utop2nei  21343  utop3cls  21344  isucn2  21372  ucnima  21374  ucncn  21378  fmucnd  21385  trcfilu  21387  comet  21606  metustexhalf  21649  metust  21651  metustbl  21659  psmetutop  21660  nrmmetd  21667  reconnlem1  21922  reconnlem2  21923  fsumcn  21980  cmetcaulem  22336  iscmet3lem1  22339  iscmet3lem2  22340  bcthlem5  22374  rrxdstprj1  22441  minveclem4  22452  minveclem4OLD  22464  ovolfiniun  22532  itg1addlem4  22736  itg1addlem5  22737  itgsplitioo  22874  c1liplem1  23027  dvfsumlem1  23057  plyeq0lem  23243  quotcan  23341  psercnlem1  23459  cxplea  23720  birthdaylem3  23958  musumsum  24200  dvdsmulf1o  24202  dchrelbas4  24250  dchrhash  24278  2sqlem8a  24378  2sqlem8  24379  chto1ub  24393  vmadivsum  24399  dchrisumlem1  24406  dchrvmasumlem2  24415  dchrvmasumiflem1  24418  rpvmasum2  24429  mulog2sumlem2  24452  selberg2lem  24467  pntrmax  24481  pntpbnd1  24503  pntlemb  24514  pntlemj  24520  ercgrg  24641  tgcgr4  24655  motcgr  24660  tglineeltr  24755  colline  24773  miriso  24794  midexlem  24816  perpneq  24838  foot  24843  f1otrg  24980  f1otrge  24981  axcontlem9  25081  uhgraun  25117  umgraun  25134  2wlklemA  25363  2wlklemB  25364  2wlklemC  25365  constr3trllem3  25459  vdgrun  25708  vdgrfiun  25709  eupap1  25783  nmblolbii  26521  minvecolem3  26599  minvecolem4  26603  minvecolem3OLD  26609  minvecolem4OLD  26613  htthlem  26651  bcs2  26916  nmopub2tALT  27643  nmfnleub2  27660  eighmorth  27698  nmophmi  27765  nmopcoadji  27835  hstle  27964  atcvat3i  28130  disjxpin  28275  off2  28318  xppreima2  28325  fgreu  28349  1stpreimas  28361  padct  28382  resf1o  28390  fpwrelmap  28393  xrofsup  28428  eliccelico  28434  elicoelioo  28435  iocinif  28438  difioo  28439  2sqcoprm  28483  2sqmod  28484  ressprs  28491  tleile  28497  xrge0addgt0  28528  xrge0adddir  28529  omndmul3  28550  archirng  28579  archirngz  28580  gsumle  28616  orngmul  28640  1smat1  28704  madjusmdetlem2  28728  qtophaus  28737  locfinref  28742  metideq  28770  sqsscirc2  28789  tpr2rico  28792  fmcncfil  28811  lmxrge0  28832  lmdvg  28833  qqhval2lem  28859  qqhf  28864  qqhnm  28868  esumle  28953  gsumesum  28954  esumlef  28957  esumrnmpt2  28963  esumpcvgval  28973  esum2d  28988  ofcf  28998  ldsysgenld  29056  ldgenpisyslem1  29059  unelros  29067  difelros  29068  inelsros  29074  diffiunisros  29075  imambfm  29157  omssubadd  29201  omssubaddOLD  29205  inelcarsg  29216  carsgsigalem  29220  carsggect  29223  carsgclctunlem2  29224  oddpwdc  29260  eulerpartlems  29266  eulerpartlemb  29274  eulerpartlemt  29277  iwrdsplit  29293  sseqfn  29296  sseqf  29298  sseqfres  29299  ballotlemfc0  29398  ballotlemfcc  29399  ballotlemfrcn0  29435  ballotlemfrcn0OLD  29473  sgnsub  29488  plymulx0  29508  signsplypnf  29511  signsvtn0  29531  signstfvneq0  29533  signsvtp  29544  signsvtn  29545  bnj927  29652  bnj1536  29737  bnj1001  29841  bnj1280  29901  cvxscon  30038  elmrsubrn  30230  nobndup  30660  nobnddown  30661  neibastop3  31089  finxpsuclem  31859  poimirlem16  32020  poimirlem19  32023  poimirlem20  32024  poimirlem29  32033  mblfinlem3  32043  itg2addnclem3  32059  ftc1cnnclem  32079  lautlt  33727  lautcvr  33728  lauteq  33731  lautco  33733  ltrncl  33761  ltrncnvleN  33766  trljat2  33804  cdlemc6  33833  cdleme20c  33949  cdleme20j  33956  cdleme22e  33982  cdleme22eALTN  33983  cdlemg7aN  34263  cdlemg12e  34285  cdlemg17dALTN  34302  cdlemh  34455  cdlemkfid1N  34559  dibglbN  34805  diblss  34809  diclspsn  34833  dih1  34925  dihglbcpreN  34939  dihmeetlem4preN  34945  lcfrlem19  35200  mapfzcons  35629  mzpcl34  35644  mzpindd  35659  mzpsubst  35661  diophrw  35672  diophren  35727  irrapxlem1  35737  pellexlem5  35748  acongrep  35901  pwssplit4  36018  phisum  36147  brtrclfv2  36390  4an4132  36925  mulltgt0  37406  fnchoice  37413  3adantlr3  37425  3adantll2  37427  3adantll3  37428  uzwo4  37451  disjf1o  37537  supxrgelem  37647  infleinflem2  37681  fmuldfeq  37758  mccl  37775  limccog  37797  limcrecl  37806  lptioo1  37809  islpcn  37816  limsupre  37818  limsupreOLD  37819  neglimc  37825  0ellimcdiv  37827  limclner  37829  icccncfext  37862  fprodcncf  37876  dvnmptdivc  37910  dvnmul  37915  dvmptfprod  37917  dvnprodlem3  37920  stoweidlem25  37997  stoweidlem34  38007  stoweidlem38  38011  stoweidlem44  38017  stoweidlem48  38021  stoweidlem49  38022  stoweidlem59  38032  stoweidlem60  38033  wallispilem4  38042  stirlinglem5  38052  dirkercncflem2  38078  fourierdlem39  38121  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem46  38128  fourierdlem47  38129  fourierdlem48  38130  fourierdlem50  38132  fourierdlem51  38133  fourierdlem64  38146  fourierdlem73  38155  fourierdlem74  38156  fourierdlem77  38159  fourierdlem80  38162  fourierdlem87  38169  fourierdlem94  38176  fourierdlem103  38185  fourierdlem104  38186  etransclem32  38243  sge0cl  38337  sge0f1o  38338  nnfoctbdjlem  38409  ismeannd  38421  omeiunltfirp  38459  hoicvr  38488  ovncvrrp  38504  hoidmvlelem2  38536  hoidmvlelem5  38539  hspdifhsp  38556  hoiqssbllem2  38563  hspmbllem2  38567  fdisjdmun  38775  uspgr1ewop  39487  nbupgrres  39602  1wlkp1  39877  uspgrn2crct  39986  crctcsh1wlkn0lem5  39992  3trlond  40087  3pthond  40089  3spthond  40091  uhgun  40200  lincresunit2  40779  nnpw2pmod  40902  dignn0flhalflem1  40934  dignn0flhalf  40937
  Copyright terms: Public domain W3C validator