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

Theorem syl12anc 1262
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 537 . 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 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:  syl22anc  1265  raaan  3907  raaanv  3908  soltmin  5255  xpdifid  5284  f1dom3fv3dif  6183  f1prex  6197  cocan1  6204  fliftfun  6220  soisores  6233  soisoi  6234  isopolem  6251  f1oiso2  6258  weniso  6260  caovcld  6476  caovcomd  6479  onminex  6648  tfrlem12  7118  omeulem1  7294  oaabs2  7357  omabs  7359  erov  7471  findcard2d  7822  frfi  7825  finsschain  7890  suplub2  7984  supmaxOLD  7992  supgtoreq  7995  supisolem  7998  ordiso2  8039  ordtypelem7  8048  wemaplem2  8071  wemapsolem  8074  cantnflt  8185  cantnfp1lem3  8193  cantnflem1b  8199  cantnflem1  8202  wemapwe  8210  cnfcomlem  8212  cnfcom  8213  cnfcom3lem  8216  infxpenlem  8452  fseqenlem1  8462  dfac12lem2  8581  infpssrlem4  8743  enfin2i  8758  isf34lem7  8816  isf34lem6  8817  fin1a2lem7  8843  fin1a2lem10  8846  fin1a2lem11  8847  fin1a2lem13  8849  ttukeylem6  8951  ttukeylem7  8952  iundom2g  8972  fpwwe2lem6  9067  fpwwe2lem7  9068  fpwwe2lem9  9070  fpwwe2lem12  9073  fpwwe2  9075  canthnumlem  9080  canthwelem  9082  canthp1lem2  9085  pwfseqlem4  9094  inar1  9207  intgru  9246  distrlem4pr  9458  conjmul  10331  lediv12a  10506  recp1lt1  10511  cju  10612  gtndiv  11020  zsupss  11260  uzsupss  11263  icc0  11691  iccssioo2  11714  fzrev3  11868  elfz1b  11871  ico01fl0  12059  fldiv  12093  modabs  12136  modltm1p1mod  12148  modifeq2int  12158  seqcaopr  12256  seqf1olem1  12258  seqof2  12277  crreczi  12403  seqcoll  12631  seqcoll2  12632  hashtpg  12645  swrdccat3b  12854  sqrlem2  13307  resqrex  13314  abs1m  13398  isercoll  13730  zsum  13783  fsum2dlem  13830  fsumcom2  13834  fprod2dlem  14033  fprodcom2  14037  efsub  14153  bitsinv2  14416  sqgcd  14525  qredeu  14663  pcpremul  14792  pceulem  14794  pczpre  14796  pcdiv  14801  pcqmul  14802  pcqdiv  14806  pcexp  14808  pcdvdsb  14817  pcneg  14822  pcdvdstr  14824  pcgcd1  14825  pc2dvds  14827  pcz  14829  pcaddlem  14832  pcadd  14833  qexpz  14845  expnprm  14846  infpnlem2  14854  ramub2  14970  ramub1lem1  14983  f1ocpbllem  15429  f1ovscpbl  15431  mreexexlem3d  15551  mreexexlem4d  15552  fthi  15822  ipodrsima  16410  mndpropd  16561  grpsubpropd2  16756  ghmf1  16910  symgfvne  17028  f1omvdmvd  17083  f1otrspeq  17087  pmtrdifwrdel  17125  pmtrdifwrdel2  17126  psgnunilem2  17135  psgnunilem3  17136  psgnvalii  17149  odf1  17212  lsmpropd  17326  gsummptshft  17568  dprdf1o  17664  pgpfac1lem3  17709  pgpfac1lem5  17711  pgpfaclem1  17713  ablfaclem2  17718  srgbinomlem3  17774  ringpropd  17811  f1rhm0to0  17967  lmodprop2d  18149  lsspropd  18239  lmhmpropd  18295  lbspropd  18321  lbsextlem3  18382  lidlsubclOLD  18439  assapropd  18550  psrass1  18628  psrass23l  18631  psrass23  18633  mplsubrg  18663  mplmon  18686  mplmonmul  18687  mplcoe1  18688  mplbas2  18693  mplind  18724  evlslem2  18734  mpfind  18758  gsumply1subr  18826  psrplusgpropd  18828  ply1scln0  18883  ply1coeOLD  18889  iporthcom  19200  obslbs  19291  scmataddcl  19539  scmatsubcl  19540  scmatmulcl  19541  smatvscl  19547  scmatrhmcl  19551  mat1scmat  19562  smadiadetglem2  19695  cramerimplem2  19707  cramerimplem3  19708  cramerimp  19709  1pmatscmul  19724  mat2pmatf1  19751  pm2mp  19847  chmatcl  19850  chmatval  19851  chmaidscmat  19870  chfacfisf  19876  cayhamlem1  19888  cpmidgsumm2pm  19891  cpmidpmat  19895  cpmadugsumfi  19899  cpmadumatpoly  19905  cayhamlem3  19909  pptbas  20021  elcls  20087  neiint  20118  neiptopnei  20146  restbas  20172  neitr  20194  iscnp4  20277  cnconst2  20297  cnpdis  20307  cnt0  20360  cnhaus  20368  cmpcovf  20404  hauscmplem  20419  concompid  20444  2ndci  20461  2ndc1stc  20464  1stcrest  20466  2ndcctbss  20468  2ndcomap  20471  2ndcsep  20472  dis2ndc  20473  restlly  20496  islly2  20497  lly1stc  20509  dislly  20510  finlocfin  20533  dissnlocfin  20542  locfindis  20543  llycmpkgen2  20563  ptbasfi  20594  neitx  20620  ptpjopn  20625  ptcnplem  20634  upxp  20636  txlly  20649  txtube  20653  tx1stc  20663  txkgen  20665  xkococnlem  20672  kqreglem1  20754  kqreglem2  20755  kqnrmlem1  20756  kqnrmlem2  20757  hmeoimaf1o  20783  reghmph  20806  nrmhmph  20807  ordthmeolem  20814  trfil2  20900  fmfnfm  20971  hauspwpwf1  21000  fclsfnflim  21040  cnextf  21079  cnextcn  21080  tmdgsum2  21109  symgtgp  21114  subgntr  21119  opnsubg  21120  ghmcnp  21127  qustgpopn  21132  tsmsf1o  21157  tsmsxplem1  21165  tsmsxplem2  21166  tsmsxp  21167  ustexsym  21228  restutop  21250  imasdsf1olem  21386  blssexps  21439  blssex  21440  ssblex  21441  imasf1oxms  21502  blcld  21518  stdbdmopn  21531  met1stc  21534  met2ndci  21535  prdsxmslem2  21542  metcnp3  21553  cfilucfil  21572  ngptgp  21642  tgioo  21812  tgqioo  21816  zdis  21832  iccpnfhmeo  21971  xrhmeo  21972  cnheibor  21981  elpi1i  22075  cmetcusp  22319  pjthlem2  22390  ivthlem2  22401  ovolicc1  22467  ovolicc2lem3  22470  ovolicc2lem4OLD  22471  ovolicc2lem4  22472  volsup  22507  volivth  22563  vitalilem3  22566  mbflimsup  22621  mbflimsupOLD  22622  mbfi1fseqlem1  22671  mbfi1fseqlem3  22673  mbfi1fseqlem5  22675  limcnlp  22831  limcflf  22834  limciun  22847  dvmptfsum  22925  dvcnvlem  22926  dvcvx  22970  facth1  23113  elply2  23148  plypf1  23164  coeeq  23179  aaliou3lem8  23299  ulm2  23338  mtestbdd  23358  reeff1o  23400  dcubic2  23768  quart  23785  xrlimcnp  23892  amgm  23914  harmonicbnd4  23934  perfect  24157  dchrptlem1  24190  bposlem2  24211  lgsfcl2  24228  lgsdir  24256  lgsdi  24258  lgsne0  24259  dchrvmasumlem2  24334  chpdifbndlem2  24390  pntpbnd1  24422  pntpbnd2  24423  padicabv  24466  tgcgrxfr  24561  idmot  24580  legid  24630  btwnleg  24631  leg0  24635  tghilberti1  24680  mirreu3  24697  colperpex  24773  lnopp2hpgb  24803  axcgrrflx  24942  axsegconlem1  24945  axcontlem2  24993  axcontlem12  25003  eengtrkg  25013  nbgraf1olem5  25171  wwlknredwwlkn  25452  clwwlkel  25519  clwlkfclwwlk  25570  2spotiundisj  25788  numclwwlkovf2ex  25812  frgraogt3nreg  25846  subgoid  26033  subgoinv  26034  ghgrpOLD  26094  nvpi  26293  nmlno0lem  26432  fh1  27269  fh2  27270  eigposi  27487  nmlnop0iALT  27646  nmopun  27665  branmfn  27756  opsqrlem1  27791  opsqrlem6  27796  mdslmd1lem1  27976  csmdsymi  27985  atom1d  28004  chirredlem2  28042  cdj1i  28084  cdj3i  28092  fcnvgreu  28277  xrofsup  28359  2sqmod  28416  archirngz  28513  archiabllem2a  28518  gsummpt2d  28551  orngsqr  28575  ornglmullt  28578  orngrmullt  28579  metideq  28704  metider  28705  pstmfval  28707  lmxrge0  28766  qqhval2  28794  qqhf  28798  qqhghm  28800  qqhrhm  28801  esumpcvgval  28907  esum2dlem  28921  esum2d  28922  sigainb  28966  insiga  28967  ddemeas  29067  imambfm  29092  dya2icoseg  29107  dya2iocnrect  29111  eulerpartlemgvv  29217  probun  29260  ballotlemfc0  29333  ballotlemfcc  29334  sgnmul  29421  signstfvneq0  29469  erdszelem8  29929  erdszelem9  29930  erdsze2lem2  29935  cnpcon  29961  txpcon  29963  ptpcon  29964  indispcon  29965  conpcon  29966  cvxpcon  29973  cnllyscon  29976  cvmcov2  30006  cvmopnlem  30009  cvmliftmolem1  30012  cvmliftlem14  30028  cvmliftlem15  30029  cvmlift2lem13  30046  cvmlift3lem2  30051  cvmlift3lem9  30058  poseq  30498  sltres  30558  nodense  30583  nocvxmin  30585  nobndup  30594  nobnddown  30595  seglerflx  30884  seglemin  30885  btwnsegle  30889  hilbert1.1  30926  neibastop2lem  31021  bj-finsumval0  31666  relowlssretop  31730  wl-2sb6d  31852  tan2h  31901  poimirlem1  31905  poimirlem3  31907  poimirlem4  31908  poimirlem9  31913  poimirlem22  31926  poimirlem28  31932  heicant  31939  mblfinlem2  31942  itg2addnc  31960  ftc2nc  31990  dvasin  31992  sdclem1  32036  fdc  32038  istotbnd3  32067  sstotbnd  32071  prdstotbnd  32090  prdsbnd2  32091  cntotbnd  32092  rngoisocnv  32184  lsmsat  32543  islfld  32597  ps-2  33012  lplnexllnN  33098  4atlem9  33137  4atlem10a  33138  lnatexN  33313  2lnat  33318  pmapjat1  33387  lhpj1  33556  lhpm0atN  33563  4atexlemex2  33605  4atex  33610  4atex2-0aOLDN  33612  4atex2-0cOLDN  33614  lautcnvle  33623  lautj  33627  lautm  33628  idltrn  33684  cdleme01N  33756  cdleme0ex1N  33758  cdleme5  33775  cdleme9  33788  cdleme11c  33796  cdleme11g  33800  cdlemefrs29bpre0  33932  cdlemefrs29cpre1  33934  cdlemefrs32fva1  33937  cdleme32fva  33973  cdleme32fva1  33974  cdleme32fvaw  33975  cdleme32d  33980  cdleme32f  33982  cdleme35fnpq  33985  cdleme48d  34071  cdleme48gfv  34073  cdleme50ltrn  34093  trlord  34105  cdlemg4b1  34145  cdlemg4b2  34146  cdlemg13a  34187  cdlemg17a  34197  cdlemg17f  34202  erng1lem  34523  erngdvlem3  34526  erngdvlem4  34527  erng1r  34531  erngdvlem3-rN  34534  erngdvlem4-rN  34535  dva0g  34564  dialss  34583  dia0  34589  dia1N  34590  diaglbN  34592  diameetN  34593  diainN  34594  diaintclN  34595  dia1dim  34598  dia2dimlem5  34605  dia2dimlem7  34607  dia2dimlem9  34609  dia2dimlem10  34610  dia2dimlem12  34612  dia2dimlem13  34613  dvhopvadd  34630  dvhvaddass  34634  dvhopvsca  34639  tendolinv  34642  tendorinv  34643  dvhlveclem  34645  dvh0g  34648  dvheveccl  34649  dvhopN  34653  docaclN  34661  diaocN  34662  djajN  34674  dib0  34701  dib1dim  34702  dibglbN  34703  dibintclN  34704  dib1dim2  34705  diblss  34707  diblsmopel  34708  dicvaddcl  34727  dicvscacl  34728  diclspsn  34731  cdlemn4a  34736  cdlemn11c  34746  dihjustlem  34753  dihord1  34755  dihord2a  34756  dihord2b  34757  dihord2cN  34758  dihord11b  34759  dihord11c  34761  dihord2pre  34762  dihlsscpre  34771  dih1dimb  34777  dib2dim  34780  dih2dimb  34781  dih2dimbALTN  34782  dihvalcq2  34784  dihopelvalcpre  34785  dihord6apre  34793  dihord5b  34796  dihord5apre  34799  dih0  34817  dihmeetlem1N  34827  dihglblem5apreN  34828  dihglblem3N  34832  dihmeetlem2N  34836  dihglbcpreN  34837  dihmeetlem4preN  34843  dih1dimatlem0  34865  dih1dimatlem  34866  dihatlat  34871  dihatexv  34875  dihglb2  34879  dihmeet  34880  dihintcl  34881  dihmeet2  34883  doch2val2  34901  dochocss  34903  dihoml4c  34913  dochdmj1  34927  djhlj  34938  djhljjN  34939  djhjlj  34940  dihsumssj  34945  djhexmid  34948  djhlsmcl  34951  djhcvat42  34952  dihjatcclem4  34958  dihjat1lem  34965  dihsmsprn  34967  dihjat3  34969  dvh3dim2  34985  dvh3dim3N  34986  dochkr1OLDN  35016  lclkrlem2c  35046  lclkrlem2d  35047  mapdpglem23  35231  hdmap11lem2  35382  mzpcompact2lem  35562  diophrw  35570  rexrabdioph  35606  eldioph4b  35623  pellexlem5  35647  pellfund14  35716  acongtr  35798  fnwe2lem3  35880  gicabl  35927  hbtlem2  35953  hbtlem4  35955  hbtlem5  35957  dgraalem  35977  dgraalemOLD  35978  aaitgo  35998  ioounsn  36064  isprm7  36630  wessf1ornlem  37420  islptre  37639  limclner  37672  icccncfext  37705  stoweidlem1  37801  stoweidlem14  37814  stoweidlem24  37824  stoweidlem46  37847  stoweidlem57  37858  dirkercncflem2  37906  fourierdlem20  37929  fourierdlem41  37951  fourierdlem46  37956  fourierdlem48  37958  fourierdlem50  37960  fourierdlem62  37972  fourierdlem63  37973  fourierdlem64  37974  fourierdlem65  37975  fourierdlem76  37986  fourierdlem79  37989  fourierdlem103  38013  fourierdlem104  38014  etransclem47  38086  raaan2  38467  iccpartiun  38618  perfectALTV  38715  nnsum4primeseven  38765  nnsum4primesevenALTV  38766  mgmpropd  39394  lidlmmgm  39544  gsumlsscl  39789  lincsumcl  39845  lincscmcl  39846  isldepslvec2  39899  m1modmmod  39945  elbigo2  39984  relogbdivb  39994  blennnt2  40021  dignn0ldlem  40034
  Copyright terms: Public domain W3C validator