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  3911  raaanv  3912  soltmin  5256  xpdifid  5285  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  7115  omeulem1  7291  oaabs2  7354  omabs  7356  erov  7468  findcard2d  7819  frfi  7822  finsschain  7887  suplub2  7981  supmaxOLD  7989  supgtoreq  7992  supisolem  7995  ordiso2  8030  ordtypelem7  8039  wemaplem2  8062  wemapsolem  8065  cantnflt  8176  cantnfp1lem3  8184  cantnflem1b  8190  cantnflem1  8193  wemapwe  8201  cnfcomlem  8203  cnfcom  8204  cnfcom3lem  8207  infxpenlem  8443  fseqenlem1  8453  dfac12lem2  8572  infpssrlem4  8734  enfin2i  8749  isf34lem7  8807  isf34lem6  8808  fin1a2lem7  8834  fin1a2lem10  8837  fin1a2lem11  8838  fin1a2lem13  8840  ttukeylem6  8942  ttukeylem7  8943  iundom2g  8963  fpwwe2lem6  9059  fpwwe2lem7  9060  fpwwe2lem9  9062  fpwwe2lem12  9065  fpwwe2  9067  canthnumlem  9072  canthwelem  9074  canthp1lem2  9077  pwfseqlem4  9086  inar1  9199  intgru  9238  distrlem4pr  9450  conjmul  10323  lediv12a  10499  recp1lt1  10504  cju  10605  gtndiv  11013  zsupss  11253  uzsupss  11256  icc0  11684  iccssioo2  11707  fzrev3  11859  elfz1b  11862  ico01fl0  12050  fldiv  12084  modabs  12127  modltm1p1mod  12139  modifeq2int  12149  seqcaopr  12247  seqf1olem1  12249  seqof2  12268  crreczi  12394  seqcoll  12621  seqcoll2  12622  hashtpg  12632  swrdccat3b  12837  sqrlem2  13286  resqrex  13293  abs1m  13377  isercoll  13709  zsum  13762  fsum2dlem  13809  fsumcom2  13813  fprod2dlem  14012  fprodcom2  14016  efsub  14132  bitsinv2  14391  sqgcd  14497  qredeu  14626  pcpremul  14747  pceulem  14749  pczpre  14751  pcdiv  14756  pcqmul  14757  pcqdiv  14761  pcexp  14763  pcdvdsb  14772  pcneg  14777  pcdvdstr  14779  pcgcd1  14780  pc2dvds  14782  pcz  14784  pcaddlem  14787  pcadd  14788  qexpz  14800  expnprm  14801  infpnlem2  14809  ramub2  14925  ramub1lem1  14938  f1ocpbllem  15372  f1ovscpbl  15374  mreexexlem3d  15494  mreexexlem4d  15495  fthi  15765  ipodrsima  16353  mndpropd  16504  grpsubpropd2  16699  ghmf1  16853  symgfvne  16971  f1omvdmvd  17026  f1otrspeq  17030  pmtrdifwrdel  17068  pmtrdifwrdel2  17069  psgnunilem2  17078  psgnunilem3  17079  psgnvalii  17092  odf1  17142  lsmpropd  17253  gsummptshft  17495  dprdf1o  17591  pgpfac1lem3  17636  pgpfac1lem5  17638  pgpfaclem1  17640  ablfaclem2  17645  srgbinomlem3  17701  ringpropd  17738  f1rhm0to0  17894  lmodprop2d  18076  lsspropd  18166  lmhmpropd  18222  lbspropd  18248  lbsextlem3  18309  lidlsubclOLD  18366  assapropd  18477  psrass1  18555  psrass23l  18558  psrass23  18560  mplsubrg  18590  mplmon  18613  mplmonmul  18614  mplcoe1  18615  mplbas2  18620  mplind  18651  evlslem2  18661  mpfind  18685  gsumply1subr  18753  psrplusgpropd  18755  ply1scln0  18810  ply1coeOLD  18816  iporthcom  19124  obslbs  19215  scmataddcl  19463  scmatsubcl  19464  scmatmulcl  19465  smatvscl  19471  scmatrhmcl  19475  mat1scmat  19486  smadiadetglem2  19619  cramerimplem2  19631  cramerimplem3  19632  cramerimp  19633  1pmatscmul  19648  mat2pmatf1  19675  pm2mp  19771  chmatcl  19774  chmatval  19775  chmaidscmat  19794  chfacfisf  19800  cayhamlem1  19812  cpmidgsumm2pm  19815  cpmidpmat  19819  cpmadugsumfi  19823  cpmadumatpoly  19829  cayhamlem3  19833  pptbas  19945  elcls  20011  neiint  20042  neiptopnei  20070  restbas  20096  neitr  20118  iscnp4  20201  cnconst2  20221  cnpdis  20231  cnt0  20284  cnhaus  20292  cmpcovf  20328  hauscmplem  20343  concompid  20368  2ndci  20385  2ndc1stc  20388  1stcrest  20390  2ndcctbss  20392  2ndcomap  20395  2ndcsep  20396  dis2ndc  20397  restlly  20420  islly2  20421  lly1stc  20433  dislly  20434  finlocfin  20457  dissnlocfin  20466  locfindis  20467  llycmpkgen2  20487  ptbasfi  20518  neitx  20544  ptpjopn  20549  ptcnplem  20558  upxp  20560  txlly  20573  txtube  20577  tx1stc  20587  txkgen  20589  xkococnlem  20596  kqreglem1  20678  kqreglem2  20679  kqnrmlem1  20680  kqnrmlem2  20681  hmeoimaf1o  20707  reghmph  20730  nrmhmph  20731  ordthmeolem  20738  trfil2  20824  fmfnfm  20895  hauspwpwf1  20924  fclsfnflim  20964  cnextf  21003  cnextcn  21004  tmdgsum2  21033  symgtgp  21038  subgntr  21043  opnsubg  21044  ghmcnp  21051  qustgpopn  21056  tsmsf1o  21081  tsmsxplem1  21089  tsmsxplem2  21090  tsmsxp  21091  ustexsym  21152  restutop  21174  imasdsf1olem  21310  blssexps  21363  blssex  21364  ssblex  21365  imasf1oxms  21426  blcld  21442  stdbdmopn  21455  met1stc  21458  met2ndci  21459  prdsxmslem2  21466  metcnp3  21477  cfilucfil  21496  ngptgp  21566  tgioo  21716  tgqioo  21720  zdis  21736  iccpnfhmeo  21860  xrhmeo  21861  cnheibor  21870  elpi1i  21961  cmetcusp  22205  pjthlem2  22264  ivthlem2  22275  ovolicc1  22338  ovolicc2lem3  22341  ovolicc2lem4  22342  volsup  22377  volivth  22433  vitalilem3  22436  mbflimsup  22491  mbflimsupOLD  22492  mbfi1fseqlem1  22541  mbfi1fseqlem3  22543  mbfi1fseqlem5  22545  limcnlp  22701  limcflf  22704  limciun  22717  dvmptfsum  22795  dvcnvlem  22796  dvcvx  22840  facth1  22981  elply2  23009  plypf1  23025  coeeq  23040  aaliou3lem8  23157  ulm2  23196  mtestbdd  23216  reeff1o  23258  dcubic2  23626  quart  23643  xrlimcnp  23750  amgm  23772  harmonicbnd4  23792  perfect  24013  dchrptlem1  24046  bposlem2  24067  lgsfcl2  24084  lgsdir  24112  lgsdi  24114  lgsne0  24115  dchrvmasumlem2  24190  chpdifbndlem2  24246  pntpbnd1  24278  pntpbnd2  24279  padicabv  24322  tgcgrxfr  24416  idmot  24433  legid  24483  btwnleg  24484  leg0  24488  tghilberti1  24532  mirreu3  24550  colperpex  24623  lnopp2hpgb  24652  axcgrrflx  24781  axsegconlem1  24784  axcontlem2  24832  axcontlem12  24842  eengtrkg  24852  nbgraf1olem5  25009  wwlknredwwlkn  25290  clwwlkel  25357  clwlkfclwwlk  25408  2spotiundisj  25626  numclwwlkovf2ex  25650  frgraogt3nreg  25684  subgoid  25871  subgoinv  25872  ghgrpOLD  25932  nvpi  26131  nmlno0lem  26270  fh1  27097  fh2  27098  eigposi  27315  nmlnop0iALT  27474  nmopun  27493  branmfn  27584  opsqrlem1  27619  opsqrlem6  27624  mdslmd1lem1  27804  csmdsymi  27813  atom1d  27832  chirredlem2  27870  cdj1i  27912  cdj3i  27920  fcnvgreu  28106  xrofsup  28180  2sqmod  28238  archirngz  28335  archiabllem2a  28340  gsummpt2d  28373  orngsqr  28397  ornglmullt  28400  orngrmullt  28401  metideq  28526  metider  28527  pstmfval  28529  lmxrge0  28588  qqhval2  28616  qqhf  28620  qqhghm  28622  qqhrhm  28623  esumpcvgval  28729  esum2dlem  28743  esum2d  28744  sigainb  28788  insiga  28789  ddemeas  28889  imambfm  28914  dya2icoseg  28929  dya2iocnrect  28933  eulerpartlemgvv  29026  probun  29069  ballotlemfc0  29142  ballotlemfcc  29143  sgnmul  29192  signstfvneq0  29240  erdszelem8  29700  erdszelem9  29701  erdsze2lem2  29706  cnpcon  29732  txpcon  29734  ptpcon  29735  indispcon  29736  conpcon  29737  cvxpcon  29744  cnllyscon  29747  cvmcov2  29777  cvmopnlem  29780  cvmliftmolem1  29783  cvmliftlem14  29799  cvmliftlem15  29800  cvmlift2lem13  29817  cvmlift3lem2  29822  cvmlift3lem9  29829  poseq  30269  sltres  30329  nodense  30354  nocvxmin  30356  nobndup  30365  nobnddown  30366  seglerflx  30655  seglemin  30656  btwnsegle  30660  hilbert1.1  30697  neibastop2lem  30792  bj-finsumval0  31438  relowlssretop  31491  wl-2sb6d  31586  tan2h  31631  poimirlem1  31635  poimirlem3  31637  poimirlem4  31638  poimirlem9  31643  poimirlem22  31656  poimirlem28  31662  heicant  31669  mblfinlem2  31672  itg2addnc  31690  ftc2nc  31720  dvasin  31722  sdclem1  31766  fdc  31768  istotbnd3  31797  sstotbnd  31801  prdstotbnd  31820  prdsbnd2  31821  cntotbnd  31822  rngoisocnv  31914  lsmsat  32273  islfld  32327  ps-2  32742  lplnexllnN  32828  4atlem9  32867  4atlem10a  32868  lnatexN  33043  2lnat  33048  pmapjat1  33117  lhpj1  33286  lhpm0atN  33293  4atexlemex2  33335  4atex  33340  4atex2-0aOLDN  33342  4atex2-0cOLDN  33344  lautcnvle  33353  lautj  33357  lautm  33358  idltrn  33414  cdleme01N  33486  cdleme0ex1N  33488  cdleme5  33505  cdleme9  33518  cdleme11c  33526  cdleme11g  33530  cdlemefrs29bpre0  33662  cdlemefrs29cpre1  33664  cdlemefrs32fva1  33667  cdleme32fva  33703  cdleme32fva1  33704  cdleme32fvaw  33705  cdleme32d  33710  cdleme32f  33712  cdleme35fnpq  33715  cdleme48d  33801  cdleme48gfv  33803  cdleme50ltrn  33823  trlord  33835  cdlemg4b1  33875  cdlemg4b2  33876  cdlemg13a  33917  cdlemg17a  33927  cdlemg17f  33932  erng1lem  34253  erngdvlem3  34256  erngdvlem4  34257  erng1r  34261  erngdvlem3-rN  34264  erngdvlem4-rN  34265  dva0g  34294  dialss  34313  dia0  34319  dia1N  34320  diaglbN  34322  diameetN  34323  diainN  34324  diaintclN  34325  dia1dim  34328  dia2dimlem5  34335  dia2dimlem7  34337  dia2dimlem9  34339  dia2dimlem10  34340  dia2dimlem12  34342  dia2dimlem13  34343  dvhopvadd  34360  dvhvaddass  34364  dvhopvsca  34369  tendolinv  34372  tendorinv  34373  dvhlveclem  34375  dvh0g  34378  dvheveccl  34379  dvhopN  34383  docaclN  34391  diaocN  34392  djajN  34404  dib0  34431  dib1dim  34432  dibglbN  34433  dibintclN  34434  dib1dim2  34435  diblss  34437  diblsmopel  34438  dicvaddcl  34457  dicvscacl  34458  diclspsn  34461  cdlemn4a  34466  cdlemn11c  34476  dihjustlem  34483  dihord1  34485  dihord2a  34486  dihord2b  34487  dihord2cN  34488  dihord11b  34489  dihord11c  34491  dihord2pre  34492  dihlsscpre  34501  dih1dimb  34507  dib2dim  34510  dih2dimb  34511  dih2dimbALTN  34512  dihvalcq2  34514  dihopelvalcpre  34515  dihord6apre  34523  dihord5b  34526  dihord5apre  34529  dih0  34547  dihmeetlem1N  34557  dihglblem5apreN  34558  dihglblem3N  34562  dihmeetlem2N  34566  dihglbcpreN  34567  dihmeetlem4preN  34573  dih1dimatlem0  34595  dih1dimatlem  34596  dihatlat  34601  dihatexv  34605  dihglb2  34609  dihmeet  34610  dihintcl  34611  dihmeet2  34613  doch2val2  34631  dochocss  34633  dihoml4c  34643  dochdmj1  34657  djhlj  34668  djhljjN  34669  djhjlj  34670  dihsumssj  34675  djhexmid  34678  djhlsmcl  34681  djhcvat42  34682  dihjatcclem4  34688  dihjat1lem  34695  dihsmsprn  34697  dihjat3  34699  dvh3dim2  34715  dvh3dim3N  34716  dochkr1OLDN  34746  lclkrlem2c  34776  lclkrlem2d  34777  mapdpglem23  34961  hdmap11lem2  35112  mzpcompact2lem  35292  diophrw  35300  rexrabdioph  35336  eldioph4b  35353  pellexlem5  35377  pellfund14  35442  acongtr  35524  fnwe2lem3  35606  gicabl  35653  hbtlem2  35679  hbtlem4  35681  hbtlem5  35683  dgraalem  35700  aaitgo  35717  ioounsn  35783  isprm7  36287  wessf1ornlem  37072  islptre  37261  limclner  37294  icccncfext  37327  stoweidlem1  37420  stoweidlem14  37433  stoweidlem24  37443  stoweidlem46  37466  stoweidlem57  37477  dirkercncflem2  37525  fourierdlem20  37548  fourierdlem41  37569  fourierdlem46  37574  fourierdlem48  37576  fourierdlem50  37578  fourierdlem62  37590  fourierdlem63  37591  fourierdlem64  37592  fourierdlem65  37593  fourierdlem76  37604  fourierdlem79  37607  fourierdlem103  37631  fourierdlem104  37632  etransclem47  37703  raaan2  37977  iccpartiun  38128  perfectALTV  38225  nnsum4primeseven  38275  nnsum4primesevenALTV  38276  mgmpropd  38523  lidlmmgm  38673  gsumlsscl  38918  lincsumcl  38974  lincscmcl  38975  isldepslvec2  39028  m1modmmod  39075  elbigo2  39114  relogbdivb  39124  blennnt2  39151  dignn0ldlem  39164
  Copyright terms: Public domain W3C validator