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

Theorem syl21anc 1263
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 536 . 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 370
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 188  df-an 372
This theorem is referenced by:  wereu2  4842  brcogw  5014  funprg  5641  funtpg  5642  fnunsn  5692  fresaun  5762  fvun1  5943  iinpreima  6016  ftpg  6080  fsnunf  6108  f1prex  6188  soisores  6224  isotr  6233  off  6551  caofrss  6569  caonncan  6574  fvmpt2curryd  7017  oaf1o  7263  omeulem1  7282  oeordi  7287  oelimcl  7300  oeeulem  7301  oeeui  7302  oaabs2  7345  omabs  7347  pmresg  7498  ralxpmap  7520  domunsncan  7669  mapunen  7738  sucdom2  7765  unxpdom2  7777  sucxpdom  7778  ac6sfi  7812  unblem4  7823  fodomfi  7847  hartogslem1  8048  brwdom2  8079  cantnflt  8167  cantnflem3  8186  cantnflem4  8187  cnfcomlem  8194  cnfcom  8195  infxpenlem  8434  infxpenc  8438  fseqenlem1  8444  pwsdompw  8623  cfeq0  8675  cofsmo  8688  cfsmolem  8689  ssfin4  8729  hsmexlem4  8848  hsmexlem5  8849  axdc3lem2  8870  axdc3lem4  8872  fpwwe2  9057  wunpr  9123  mulclpi  9307  mulcanenq  9374  distrlem4pr  9440  prlem934  9447  prlem936  9461  divge0d  11367  fseq1p1m1  11855  elfznelfzob  12001  seqcaopr2  12235  facavg  12472  hashimarn  12594  cats1un  12806  f1oun2prg  12970  sqrtdiv  13297  sqrtdivd  13453  mulcn2  13626  o1of2  13643  fsumsplit  13773  sumsplit  13796  isumless  13870  demoivreALT  14222  rpnnen2lem11  14244  gcdnncl  14444  isprm5  14611  qredeu  14624  rpexp  14632  rpdvds  14636  divnumden  14657  divdenle  14658  phimullem  14685  pythagtriplem4  14721  pythagtriplem8  14725  pythagtriplem9  14726  pcgcd1  14778  sumhash  14793  fldivp1  14794  pockthlem  14801  ssc2  15671  estrreslem1  15966  mndpropd  16506  grpidssd  16674  grpinvssd  16675  issubg2  16776  isnsg3  16795  eqgid  16813  gass  16899  symgextres  17010  gsmsymgreqlem2  17016  sylow1lem5  17182  sylow2alem2  17198  sylow3lem3  17209  efgredlemd  17322  efgredlem  17325  frgpnabllem1  17437  frgpnabllem2  17438  subgdmdprd  17595  ablfacrplem  17626  kerf1hrm  17899  issrngd  18017  lmodprop2d  18078  lsspropd  18168  pwssplit1  18210  lspvadd  18247  mplsubglem  18586  mplind  18653  znidomb  19056  znrrg  19060  lindfind  19298  lindsind  19299  mat1ghm  19432  mdetunilem1  19561  mdetunilem3  19563  mdetunilem4  19564  mdetunilem9  19569  cramerimplem2  19633  mat2pmatlin  19683  monmatcollpw  19727  cpmadugsumlemF  19824  mretopd  20032  neiptopnei  20072  neitr  20120  ufilen  20869  flimrest  20922  flimclslem  20923  fclsrest  20963  cnextcn  21006  haustsms2  21075  tsmsxplem2  21092  trust  21168  utoptop  21173  restutop  21176  ustuqtop4  21183  utopsnneiplem  21186  utop2nei  21189  utop3cls  21190  isucn2  21218  ucnima  21220  ucncn  21224  fmucnd  21231  trcfilu  21233  comet  21452  metustexhalf  21495  metust  21497  metustbl  21505  psmetutop  21506  nrmmetd  21513  reconnlem1  21748  reconnlem2  21749  fsumcn  21791  cmetcaulem  22144  iscmet3lem1  22147  iscmet3lem2  22148  bcthlem5  22182  rrxdstprj1  22249  minveclem4  22260  ovolfiniun  22328  itg1addlem4  22531  itg1addlem5  22532  itgsplitioo  22669  c1liplem1  22822  dvfsumlem1  22852  plyeq0lem  23029  quotcan  23127  psercnlem1  23242  cxplea  23503  birthdaylem3  23741  musumsum  23981  dvdsmulf1o  23983  dchrelbas4  24031  dchrhash  24059  2sqlem8a  24159  2sqlem8  24160  chto1ub  24174  vmadivsum  24180  dchrisumlem1  24187  dchrvmasumlem2  24196  dchrvmasumiflem1  24199  rpvmasum2  24210  mulog2sumlem2  24233  selberg2lem  24248  pntrmax  24262  pntpbnd1  24284  pntlemb  24295  pntlemj  24301  ercgrg  24421  motcgr  24438  tglineeltr  24532  colline  24551  miriso  24571  midexlem  24591  perpneq  24613  foot  24618  f1otrg  24744  f1otrge  24745  axcontlem9  24845  uhgraun  24881  umgraun  24898  2wlklemA  25126  2wlklemB  25127  2wlklemC  25128  constr3trllem3  25222  vdgrun  25471  vdgrfiun  25472  eupap1  25546  nmblolbii  26282  minvecolem3  26360  minvecolem4  26364  htthlem  26402  bcs2  26667  nmopub2tALT  27394  nmfnleub2  27411  eighmorth  27449  nmophmi  27516  nmopcoadji  27586  hstle  27715  atcvat3i  27881  disjxpin  28034  off2  28079  xppreima2  28086  fgreu  28111  1stpreimas  28123  padct  28147  resf1o  28155  fpwrelmap  28158  xrofsup  28186  eliccelico  28192  elicoelioo  28193  iocinif  28196  difioo  28197  2sqcoprm  28243  2sqmod  28244  ressprs  28251  tleile  28257  xrge0addgt0  28289  xrge0adddir  28290  omndmul3  28311  archirng  28340  archirngz  28341  gsumle  28377  orngmul  28402  1smat1  28466  madjusmdetlem2  28490  qtophaus  28499  locfinref  28504  metideq  28532  sqsscirc2  28551  tpr2rico  28554  fmcncfil  28573  lmxrge0  28594  lmdvg  28595  qqhval2lem  28621  qqhf  28626  qqhnm  28630  esumle  28715  gsumesum  28716  esumlef  28719  esumrnmpt2  28725  esumpcvgval  28735  esum2d  28750  ofcf  28760  ldsysgenld  28818  ldgenpisyslem1  28821  unelros  28829  difelros  28830  inelsros  28836  diffiunisros  28837  imambfm  28920  omssubadd  28958  inelcarsg  28969  carsgsigalem  28973  carsggect  28976  carsgclctunlem2  28977  oddpwdc  29010  eulerpartlems  29016  eulerpartlemb  29024  eulerpartlemt  29027  iwrdsplit  29043  sseqfn  29046  sseqf  29048  sseqfres  29049  ballotlemfc0  29148  ballotlemfcc  29149  ballotlemfrcn0  29185  sgnsub  29200  plymulx0  29221  signsplypnf  29224  signsvtn0  29244  signstfvneq0  29246  signsvtp  29257  signsvtn  29258  bnj927  29365  bnj1536  29450  bnj1001  29554  bnj1280  29614  cvxscon  29751  elmrsubrn  29943  nobndup  30371  nobnddown  30372  neibastop3  30800  poimirlem16  31660  poimirlem19  31663  poimirlem20  31664  poimirlem29  31673  mblfinlem3  31683  itg2addnclem3  31699  ftc1cnnclem  31719  lautlt  33365  lautcvr  33366  lauteq  33369  lautco  33371  ltrncl  33399  ltrncnvleN  33404  trljat2  33442  cdlemc6  33471  cdleme20c  33587  cdleme20j  33594  cdleme22e  33620  cdleme22eALTN  33621  cdlemg7aN  33901  cdlemg12e  33923  cdlemg17dALTN  33940  cdlemh  34093  cdlemkfid1N  34197  dibglbN  34443  diblss  34447  diclspsn  34471  dih1  34563  dihglbcpreN  34577  dihmeetlem4preN  34583  lcfrlem19  34838  mapfzcons  35267  mzpcl34  35282  mzpindd  35297  mzpsubst  35299  diophrw  35310  diophren  35365  irrapxlem1  35376  pellexlem5  35387  acongrep  35540  pwssplit4  35657  phisum  35779  brtrclfv2  35962  4an4132  36496  mulltgt0  36987  fnchoice  36994  3adantlr3  37006  3adantll2  37008  3adantll3  37009  uzwo4  37037  disjf1o  37093  supxrgelem  37173  fmuldfeq  37237  mccl  37254  limccog  37276  limcrecl  37285  lptioo1  37288  islpcn  37295  limsupre  37297  limsupreOLD  37298  neglimc  37304  0ellimcdiv  37306  limclner  37308  icccncfext  37341  fprodcncf  37355  dvnmptdivc  37386  dvnmul  37391  dvmptfprod  37393  dvnprodlem3  37396  stoweidlem25  37458  stoweidlem34  37468  stoweidlem38  37472  stoweidlem44  37478  stoweidlem48  37482  stoweidlem49  37483  stoweidlem59  37493  stoweidlem60  37494  wallispilem4  37503  stirlinglem5  37513  dirkercncflem2  37539  fourierdlem39  37581  fourierdlem42  37584  fourierdlem46  37588  fourierdlem47  37589  fourierdlem48  37590  fourierdlem50  37592  fourierdlem51  37593  fourierdlem64  37606  fourierdlem73  37615  fourierdlem74  37616  fourierdlem77  37619  fourierdlem80  37622  fourierdlem87  37629  fourierdlem94  37636  fourierdlem103  37645  fourierdlem104  37646  etransclem32  37702  sge0cl  37761  sge0f1o  37762  nnfoctbdjlem  37806  ismeannd  37818  omeiunltfirp  37853  uhgun  38463  lincresunit2  39044  nnpw2pmod  39168  dignn0flhalflem1  39200  dignn0flhalf  39203
  Copyright terms: Public domain W3C validator