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

Theorem syl12anc 1274
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 )
syl12anc.4  |-  ( ( ps  /\  ( ch 
/\  th ) )  ->  ta )
Assertion
Ref Expression
syl12anc  |-  ( ph  ->  ta )

Proof of Theorem syl12anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
41, 2, 3jca32 542 . 2  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
5 syl12anc.4 . 2  |-  ( ( ps  /\  ( ch 
/\  th ) )  ->  ta )
64, 5syl 17 1  |-  ( ph  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 377
This theorem is referenced by:  syl22anc  1277  raaan  3889  raaanv  3890  soltmin  5255  xpdifid  5284  f1dom3fv3dif  6193  f1prex  6207  cocan1  6214  fliftfun  6230  soisores  6243  soisoi  6244  isopolem  6261  f1oiso2  6268  weniso  6270  caovcld  6489  caovcomd  6492  onminex  6661  tfrlem12  7133  omeulem1  7309  oaabs2  7372  omabs  7374  erov  7486  findcard2d  7839  frfi  7842  finsschain  7907  suplub2  8001  supmaxOLD  8009  supgtoreq  8012  supisolem  8015  ordiso2  8056  ordtypelem7  8065  wemaplem2  8088  wemapsolem  8091  cantnflt  8203  cantnfp1lem3  8211  cantnflem1b  8217  cantnflem1  8220  wemapwe  8228  cnfcomlem  8230  cnfcom  8231  cnfcom3lem  8234  infxpenlem  8470  fseqenlem1  8481  dfac12lem2  8600  infpssrlem4  8762  enfin2i  8777  isf34lem7  8835  isf34lem6  8836  fin1a2lem7  8862  fin1a2lem10  8865  fin1a2lem11  8866  fin1a2lem13  8868  ttukeylem6  8970  ttukeylem7  8971  iundom2g  8991  fpwwe2lem6  9086  fpwwe2lem7  9087  fpwwe2lem9  9089  fpwwe2lem12  9092  fpwwe2  9094  canthnumlem  9099  canthwelem  9101  canthp1lem2  9104  pwfseqlem4  9113  inar1  9226  intgru  9265  distrlem4pr  9477  conjmul  10352  lediv12a  10527  recp1lt1  10532  cju  10633  gtndiv  11042  zsupss  11282  uzsupss  11285  icc0  11713  iccssioo2  11736  fzrev3  11890  elfz1b  11893  ico01fl0  12085  fldiv  12119  modabs  12162  modltm1p1mod  12174  modifeq2int  12184  seqcaopr  12282  seqf1olem1  12284  seqof2  12303  crreczi  12429  seqcoll  12660  seqcoll2  12661  hashtpg  12674  swrdccat3b  12889  sqrlem2  13356  resqrex  13363  abs1m  13447  isercoll  13780  zsum  13833  fsum2dlem  13880  fsumcom2  13884  fprod2dlem  14083  fprodcom2  14087  efsub  14203  bitsinv2  14466  sqgcd  14575  qredeu  14713  pcpremul  14842  pceulem  14844  pczpre  14846  pcdiv  14851  pcqmul  14852  pcqdiv  14856  pcexp  14858  pcdvdsb  14867  pcneg  14872  pcdvdstr  14874  pcgcd1  14875  pc2dvds  14877  pcz  14879  pcaddlem  14882  pcadd  14883  qexpz  14895  expnprm  14896  infpnlem2  14904  ramub2  15020  ramub1lem1  15033  f1ocpbllem  15479  f1ovscpbl  15481  mreexexlem3d  15601  mreexexlem4d  15602  fthi  15872  ipodrsima  16460  mndpropd  16611  grpsubpropd2  16806  ghmf1  16960  symgfvne  17078  f1omvdmvd  17133  f1otrspeq  17137  pmtrdifwrdel  17175  pmtrdifwrdel2  17176  psgnunilem2  17185  psgnunilem3  17186  psgnvalii  17199  odf1  17262  lsmpropd  17376  gsummptshft  17618  dprdf1o  17714  pgpfac1lem3  17759  pgpfac1lem5  17761  pgpfaclem1  17763  ablfaclem2  17768  srgbinomlem3  17824  ringpropd  17861  f1rhm0to0  18017  lmodprop2d  18199  lsspropd  18289  lmhmpropd  18345  lbspropd  18371  lbsextlem3  18432  lidlsubclOLD  18489  assapropd  18600  psrass1  18678  psrass23l  18681  psrass23  18683  mplsubrg  18713  mplmon  18736  mplmonmul  18737  mplcoe1  18738  mplbas2  18743  mplind  18774  evlslem2  18784  mpfind  18808  gsumply1subr  18876  psrplusgpropd  18878  ply1scln0  18933  ply1coeOLD  18939  iporthcom  19251  obslbs  19342  scmataddcl  19590  scmatsubcl  19591  scmatmulcl  19592  smatvscl  19598  scmatrhmcl  19602  mat1scmat  19613  smadiadetglem2  19746  cramerimplem2  19758  cramerimplem3  19759  cramerimp  19760  1pmatscmul  19775  mat2pmatf1  19802  pm2mp  19898  chmatcl  19901  chmatval  19902  chmaidscmat  19921  chfacfisf  19927  cayhamlem1  19939  cpmidgsumm2pm  19942  cpmidpmat  19946  cpmadugsumfi  19950  cpmadumatpoly  19956  cayhamlem3  19960  pptbas  20072  elcls  20138  neiint  20169  neiptopnei  20197  restbas  20223  neitr  20245  iscnp4  20328  cnconst2  20348  cnpdis  20358  cnt0  20411  cnhaus  20419  cmpcovf  20455  hauscmplem  20470  concompid  20495  2ndci  20512  2ndc1stc  20515  1stcrest  20517  2ndcctbss  20519  2ndcomap  20522  2ndcsep  20523  dis2ndc  20524  restlly  20547  islly2  20548  lly1stc  20560  dislly  20561  finlocfin  20584  dissnlocfin  20593  locfindis  20594  llycmpkgen2  20614  ptbasfi  20645  neitx  20671  ptpjopn  20676  ptcnplem  20685  upxp  20687  txlly  20700  txtube  20704  tx1stc  20714  txkgen  20716  xkococnlem  20723  kqreglem1  20805  kqreglem2  20806  kqnrmlem1  20807  kqnrmlem2  20808  hmeoimaf1o  20834  reghmph  20857  nrmhmph  20858  ordthmeolem  20865  trfil2  20951  fmfnfm  21022  hauspwpwf1  21051  fclsfnflim  21091  cnextf  21130  cnextcn  21131  tmdgsum2  21160  symgtgp  21165  subgntr  21170  opnsubg  21171  ghmcnp  21178  qustgpopn  21183  tsmsf1o  21208  tsmsxplem1  21216  tsmsxplem2  21217  tsmsxp  21218  ustexsym  21279  restutop  21301  imasdsf1olem  21437  blssexps  21490  blssex  21491  ssblex  21492  imasf1oxms  21553  blcld  21569  stdbdmopn  21582  met1stc  21585  met2ndci  21586  prdsxmslem2  21593  metcnp3  21604  cfilucfil  21623  ngptgp  21693  tgioo  21863  tgqioo  21867  zdis  21883  iccpnfhmeo  22022  xrhmeo  22023  cnheibor  22032  elpi1i  22126  cmetcusp  22370  pjthlem2  22441  ivthlem2  22452  ovolicc1  22518  ovolicc2lem3  22521  ovolicc2lem4OLD  22522  ovolicc2lem4  22523  volsup  22558  volivth  22614  vitalilem3  22617  mbflimsup  22672  mbflimsupOLD  22673  mbfi1fseqlem1  22722  mbfi1fseqlem3  22724  mbfi1fseqlem5  22726  limcnlp  22882  limcflf  22885  limciun  22898  dvmptfsum  22976  dvcnvlem  22977  dvcvx  23021  facth1  23164  elply2  23199  plypf1  23215  coeeq  23230  aaliou3lem8  23350  ulm2  23389  mtestbdd  23409  reeff1o  23451  dcubic2  23819  quart  23836  xrlimcnp  23943  amgm  23965  harmonicbnd4  23985  perfect  24208  dchrptlem1  24241  bposlem2  24262  lgsfcl2  24279  lgsdir  24307  lgsdi  24309  lgsne0  24310  dchrvmasumlem2  24385  chpdifbndlem2  24441  pntpbnd1  24473  pntpbnd2  24474  padicabv  24517  tgcgrxfr  24612  idmot  24631  legid  24681  btwnleg  24682  leg0  24686  tghilberti1  24731  mirreu3  24748  colperpex  24824  lnopp2hpgb  24854  axcgrrflx  24993  axsegconlem1  24996  axcontlem2  25044  axcontlem12  25054  eengtrkg  25064  nbgraf1olem5  25222  wwlknredwwlkn  25503  clwwlkel  25570  clwlkfclwwlk  25621  2spotiundisj  25839  numclwwlkovf2ex  25863  frgraogt3nreg  25897  subgoid  26084  subgoinv  26085  ghgrpOLD  26145  nvpi  26344  nmlno0lem  26483  fh1  27320  fh2  27321  eigposi  27538  nmlnop0iALT  27697  nmopun  27716  branmfn  27807  opsqrlem1  27842  opsqrlem6  27847  mdslmd1lem1  28027  csmdsymi  28036  atom1d  28055  chirredlem2  28093  cdj1i  28135  cdj3i  28143  fcnvgreu  28324  xrofsup  28402  2sqmod  28458  archirngz  28555  archiabllem2a  28560  gsummpt2d  28593  orngsqr  28616  ornglmullt  28619  orngrmullt  28620  metideq  28745  metider  28746  pstmfval  28748  lmxrge0  28807  qqhval2  28835  qqhf  28839  qqhghm  28841  qqhrhm  28842  esumpcvgval  28948  esum2dlem  28962  esum2d  28963  sigainb  29007  insiga  29008  ddemeas  29108  imambfm  29133  dya2icoseg  29148  dya2iocnrect  29152  eulerpartlemgvv  29258  probun  29301  ballotlemfc0  29374  ballotlemfcc  29375  sgnmul  29462  signstfvneq0  29510  erdszelem8  29970  erdszelem9  29971  erdsze2lem2  29976  cnpcon  30002  txpcon  30004  ptpcon  30005  indispcon  30006  conpcon  30007  cvxpcon  30014  cnllyscon  30017  cvmcov2  30047  cvmopnlem  30050  cvmliftmolem1  30053  cvmliftlem14  30069  cvmliftlem15  30070  cvmlift2lem13  30087  cvmlift3lem2  30092  cvmlift3lem9  30099  poseq  30540  sltres  30600  nodense  30627  nocvxmin  30629  nobndup  30638  nobnddown  30639  seglerflx  30928  seglemin  30929  btwnsegle  30933  hilbert1.1  30970  neibastop2lem  31065  bj-finsumval0  31747  relowlssretop  31811  wl-2sb6d  31933  tan2h  31982  poimirlem1  31986  poimirlem3  31988  poimirlem4  31989  poimirlem9  31994  poimirlem22  32007  poimirlem28  32013  heicant  32020  mblfinlem2  32023  itg2addnc  32041  ftc2nc  32071  dvasin  32073  sdclem1  32117  fdc  32119  istotbnd3  32148  sstotbnd  32152  prdstotbnd  32171  prdsbnd2  32172  cntotbnd  32173  rngoisocnv  32265  lsmsat  32619  islfld  32673  ps-2  33088  lplnexllnN  33174  4atlem9  33213  4atlem10a  33214  lnatexN  33389  2lnat  33394  pmapjat1  33463  lhpj1  33632  lhpm0atN  33639  4atexlemex2  33681  4atex  33686  4atex2-0aOLDN  33688  4atex2-0cOLDN  33690  lautcnvle  33699  lautj  33703  lautm  33704  idltrn  33760  cdleme01N  33832  cdleme0ex1N  33834  cdleme5  33851  cdleme9  33864  cdleme11c  33872  cdleme11g  33876  cdlemefrs29bpre0  34008  cdlemefrs29cpre1  34010  cdlemefrs32fva1  34013  cdleme32fva  34049  cdleme32fva1  34050  cdleme32fvaw  34051  cdleme32d  34056  cdleme32f  34058  cdleme35fnpq  34061  cdleme48d  34147  cdleme48gfv  34149  cdleme50ltrn  34169  trlord  34181  cdlemg4b1  34221  cdlemg4b2  34222  cdlemg13a  34263  cdlemg17a  34273  cdlemg17f  34278  erng1lem  34599  erngdvlem3  34602  erngdvlem4  34603  erng1r  34607  erngdvlem3-rN  34610  erngdvlem4-rN  34611  dva0g  34640  dialss  34659  dia0  34665  dia1N  34666  diaglbN  34668  diameetN  34669  diainN  34670  diaintclN  34671  dia1dim  34674  dia2dimlem5  34681  dia2dimlem7  34683  dia2dimlem9  34685  dia2dimlem10  34686  dia2dimlem12  34688  dia2dimlem13  34689  dvhopvadd  34706  dvhvaddass  34710  dvhopvsca  34715  tendolinv  34718  tendorinv  34719  dvhlveclem  34721  dvh0g  34724  dvheveccl  34725  dvhopN  34729  docaclN  34737  diaocN  34738  djajN  34750  dib0  34777  dib1dim  34778  dibglbN  34779  dibintclN  34780  dib1dim2  34781  diblss  34783  diblsmopel  34784  dicvaddcl  34803  dicvscacl  34804  diclspsn  34807  cdlemn4a  34812  cdlemn11c  34822  dihjustlem  34829  dihord1  34831  dihord2a  34832  dihord2b  34833  dihord2cN  34834  dihord11b  34835  dihord11c  34837  dihord2pre  34838  dihlsscpre  34847  dih1dimb  34853  dib2dim  34856  dih2dimb  34857  dih2dimbALTN  34858  dihvalcq2  34860  dihopelvalcpre  34861  dihord6apre  34869  dihord5b  34872  dihord5apre  34875  dih0  34893  dihmeetlem1N  34903  dihglblem5apreN  34904  dihglblem3N  34908  dihmeetlem2N  34912  dihglbcpreN  34913  dihmeetlem4preN  34919  dih1dimatlem0  34941  dih1dimatlem  34942  dihatlat  34947  dihatexv  34951  dihglb2  34955  dihmeet  34956  dihintcl  34957  dihmeet2  34959  doch2val2  34977  dochocss  34979  dihoml4c  34989  dochdmj1  35003  djhlj  35014  djhljjN  35015  djhjlj  35016  dihsumssj  35021  djhexmid  35024  djhlsmcl  35027  djhcvat42  35028  dihjatcclem4  35034  dihjat1lem  35041  dihsmsprn  35043  dihjat3  35045  dvh3dim2  35061  dvh3dim3N  35062  dochkr1OLDN  35092  lclkrlem2c  35122  lclkrlem2d  35123  mapdpglem23  35307  hdmap11lem2  35458  mzpcompact2lem  35638  diophrw  35646  rexrabdioph  35682  eldioph4b  35699  pellexlem5  35722  pellfund14  35791  acongtr  35873  fnwe2lem3  35955  gicabl  36002  hbtlem2  36028  hbtlem4  36030  hbtlem5  36032  dgraalem  36052  dgraalemOLD  36053  aaitgo  36073  ioounsn  36139  isprm7  36704  wessf1ornlem  37497  islptre  37737  limclner  37770  icccncfext  37803  stoweidlem1  37899  stoweidlem14  37912  stoweidlem24  37922  stoweidlem46  37945  stoweidlem57  37956  dirkercncflem2  38004  fourierdlem20  38027  fourierdlem41  38049  fourierdlem46  38054  fourierdlem48  38056  fourierdlem50  38058  fourierdlem62  38070  fourierdlem63  38071  fourierdlem64  38072  fourierdlem65  38073  fourierdlem76  38084  fourierdlem79  38087  fourierdlem103  38111  fourierdlem104  38112  etransclem47  38184  raaan2  38634  iccpartiun  38786  perfectALTV  38883  nnsum4primeseven  38933  nnsum4primesevenALTV  38934  0wlkOn  39837  0TrlOn  39840  upgr3v3e3cycl  39921  mgmpropd  40048  lidlmmgm  40198  gsumlsscl  40441  lincsumcl  40497  lincscmcl  40498  isldepslvec2  40551  m1modmmod  40597  elbigo2  40636  relogbdivb  40646  blennnt2  40673  dignn0ldlem  40686
  Copyright terms: Public domain W3C validator