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

Theorem syl12anc 1227
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 535 . 2  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
5 syl12anc.4 . 2  |-  ( ( ps  /\  ( ch 
/\  th ) )  ->  ta )
64, 5syl 16 1  |-  ( ph  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  syl22anc  1230  raaan  3922  raaanv  3923  soltmin  5396  xpdifid  5425  f1dom3fv3dif  6160  cocan1  6179  fliftfun  6195  soisores  6208  soisoi  6209  isopolem  6226  f1oiso2  6233  weniso  6235  caovcld  6453  caovcomd  6456  onminex  6627  tfrlem12  7060  omeulem1  7233  oaabs2  7296  omabs  7298  erov  7410  findcard2d  7764  frfi  7767  finsschain  7829  suplub2  7923  supmaxOLD  7928  supgtoreq  7931  supisolem  7934  ordiso2  7943  ordtypelem7  7952  wemaplem2  7975  wemapsolem  7978  cantnflt  8094  cantnfp1lem3  8102  cantnflem1b  8108  cantnflem1  8111  cantnfltOLD  8124  cantnfp1lem3OLD  8128  cantnflem1bOLD  8131  cantnflem1OLD  8134  wemapwe  8142  wemapweOLD  8143  cnfcomlem  8146  cnfcom  8147  cnfcom3lem  8150  cnfcomlemOLD  8154  cnfcomOLD  8155  cnfcom3lemOLD  8158  infxpenlem  8394  fseqenlem1  8408  dfac12lem2  8527  infpssrlem4  8689  enfin2i  8704  isf34lem7  8762  isf34lem6  8763  fin1a2lem7  8789  fin1a2lem10  8792  fin1a2lem11  8793  fin1a2lem13  8795  ttukeylem6  8897  ttukeylem7  8898  iundom2g  8918  fpwwe2lem6  9016  fpwwe2lem7  9017  fpwwe2lem9  9019  fpwwe2lem12  9022  fpwwe2  9024  canthnumlem  9029  canthwelem  9031  canthp1lem2  9034  pwfseqlem4  9043  inar1  9156  intgru  9195  distrlem4pr  9407  conjmul  10268  lediv12a  10445  recp1lt1  10450  cju  10539  gtndiv  10947  zsupss  11182  uzsupss  11185  icc0  11588  iccssioo2  11608  fzrev3  11756  elfz1b  11759  fldiv  11969  modabs  12011  addmodid  12018  modltm1p1mod  12021  modifeq2int  12031  seqcaopr  12126  seqf1olem1  12128  seqof2  12147  crreczi  12273  seqcoll  12494  seqcoll2  12495  hashtpg  12505  swrdccat3b  12703  sqrlem2  13059  resqrex  13066  abs1m  13150  isercoll  13472  zsum  13522  fsum2dlem  13567  fsumcom2  13571  fprod2dlem  13766  fprodcom2  13770  efsub  13817  bitsinv2  14075  sqgcd  14178  qredeu  14230  pcpremul  14349  pceulem  14351  pczpre  14353  pcdiv  14358  pcqmul  14359  pcqdiv  14363  pcexp  14365  pcdvdsb  14374  pcneg  14379  pcdvdstr  14381  pcgcd1  14382  pc2dvds  14384  pcz  14386  pcaddlem  14389  pcadd  14390  qexpz  14402  expnprm  14403  infpnlem2  14411  ramub2  14514  ramub1lem1  14526  f1ocpbllem  14903  f1ovscpbl  14905  mreexexlem3d  15025  mreexexlem4d  15026  fthi  15266  ipodrsima  15774  mndpropd  15925  grpsubpropd2  16120  ghmf1  16274  symgfvne  16392  f1omvdmvd  16447  f1otrspeq  16451  pmtrdifwrdel  16489  pmtrdifwrdel2  16490  psgnunilem2  16499  psgnunilem3  16500  psgnvalii  16513  odf1  16563  lsmpropd  16674  gsummptshft  16935  dprdf1o  17058  pgpfac1lem3  17107  pgpfac1lem5  17109  pgpfaclem1  17111  ablfaclem2  17116  srgbinomlem3  17172  ringpropd  17209  f1rhm0to0  17368  lmodprop2d  17551  lsspropd  17642  lmhmpropd  17698  lbspropd  17724  lbsextlem3  17785  lidlsubclOLD  17843  assapropd  17955  psrass1  18039  psrass23l  18042  psrass23  18044  mplsubrg  18081  mplmon  18104  mplmonmul  18105  mplcoe1  18106  mplbas2  18113  mplind  18146  evlslem2  18159  mpfind  18184  gsumply1subr  18254  psrplusgpropd  18256  ply1scln0  18311  ply1coeOLD  18317  iporthcom  18648  obslbs  18739  scmataddcl  18996  scmatsubcl  18997  scmatmulcl  18998  smatvscl  19004  scmatrhmcl  19008  mat1scmat  19019  smadiadetglem2  19152  cramerimplem2  19164  cramerimplem3  19165  cramerimp  19166  1pmatscmul  19181  mat2pmatf1  19208  pm2mp  19304  chmatcl  19307  chmatval  19308  chmaidscmat  19327  chfacfisf  19333  cayhamlem1  19345  cpmidgsumm2pm  19348  cpmidpmat  19352  cpmadugsumfi  19356  cpmadumatpoly  19362  cayhamlem3  19366  pptbas  19487  elcls  19552  neiint  19583  neiptopnei  19611  restbas  19637  neitr  19659  iscnp4  19742  cnconst2  19762  cnpdis  19772  cnt0  19825  cnhaus  19833  cmpcovf  19869  hauscmplem  19884  concompid  19910  2ndci  19927  2ndc1stc  19930  1stcrest  19932  2ndcctbss  19934  2ndcomap  19937  2ndcsep  19938  dis2ndc  19939  restlly  19962  islly2  19963  lly1stc  19975  dislly  19976  finlocfin  19999  dissnlocfin  20008  locfindis  20009  llycmpkgen2  20029  ptbasfi  20060  neitx  20086  ptpjopn  20091  ptcnplem  20100  upxp  20102  txlly  20115  txtube  20119  tx1stc  20129  txkgen  20131  xkococnlem  20138  kqreglem1  20220  kqreglem2  20221  kqnrmlem1  20222  kqnrmlem2  20223  hmeoimaf1o  20249  reghmph  20272  nrmhmph  20273  ordthmeolem  20280  trfil2  20366  fmfnfm  20437  hauspwpwf1  20466  fclsfnflim  20506  cnextf  20544  cnextcn  20545  tmdgsum2  20573  symgtgp  20578  subgntr  20583  opnsubg  20584  ghmcnp  20591  qustgpopn  20596  tsmsf1o  20625  tsmsxplem1  20633  tsmsxplem2  20634  tsmsxp  20635  ustexsym  20696  restutop  20718  imasdsf1olem  20854  blssexps  20907  blssex  20908  ssblex  20909  imasf1oxms  20970  blcld  20986  stdbdmopn  20999  met1stc  21002  met2ndci  21003  prdsxmslem2  21010  metcnp3  21021  cfilucfilOLD  21050  cfilucfil  21051  ngptgp  21128  tgioo  21279  tgqioo  21283  zdis  21299  iccpnfhmeo  21423  xrhmeo  21424  cnheibor  21433  elpi1i  21524  cmetcuspOLD  21771  cmetcusp  21772  pjthlem2  21831  ivthlem2  21842  ovolicc1  21905  ovolicc2lem3  21908  ovolicc2lem4  21909  volsup  21944  volivth  21994  vitalilem3  21997  mbflimsup  22051  mbfi1fseqlem1  22100  mbfi1fseqlem3  22102  mbfi1fseqlem5  22104  limcnlp  22260  limcflf  22263  limciun  22276  dvmptfsum  22354  dvcnvlem  22355  dvcvx  22399  facth1  22543  elply2  22571  plypf1  22587  coeeq  22602  aaliou3lem8  22719  ulm2  22758  mtestbdd  22778  reeff1o  22820  dcubic2  23153  quart  23170  xrlimcnp  23276  amgm  23298  harmonicbnd4  23318  perfect  23484  dchrptlem1  23517  bposlem2  23538  lgsfcl2  23555  lgsdir  23583  lgsdi  23585  lgsne0  23586  dchrvmasumlem2  23661  chpdifbndlem2  23717  pntpbnd1  23749  pntpbnd2  23750  padicabv  23793  tgcgrxfr  23887  idmot  23902  legid  23952  btwnleg  23953  leg0  23957  tghilbert1_1  23995  mirreu3  24013  colperpex  24085  lnopp2hpgb  24110  axcgrrflx  24195  axsegconlem1  24198  axcontlem2  24246  axcontlem12  24256  eengtrkg  24266  nbgraf1olem5  24423  wwlknredwwlkn  24704  clwwlkel  24771  clwlkfclwwlk  24822  2spotiundisj  25040  numclwwlkovf2ex  25064  frgraogt3nreg  25098  subgoid  25287  subgoinv  25288  ghgrpOLD  25348  nvpi  25547  nmlno0lem  25686  fh1  26514  fh2  26515  eigposi  26733  nmlnop0iALT  26892  nmopun  26911  branmfn  27002  opsqrlem1  27037  opsqrlem6  27042  mdslmd1lem1  27222  csmdsymi  27231  atom1d  27250  chirredlem2  27288  cdj1i  27330  cdj3i  27338  fcnvgreu  27492  xrofsup  27560  2sqmod  27614  archirngz  27711  archiabllem2a  27716  orngsqr  27772  ornglmullt  27775  orngrmullt  27776  metideq  27850  metider  27851  pstmfval  27853  lmxrge0  27912  qqhval2  27941  qqhf  27945  qqhghm  27947  qqhrhm  27948  esumpcvgval  28062  sigainb  28114  insiga  28115  ddemeas  28186  imambfm  28211  dya2icoseg  28226  dya2iocnrect  28230  eulerpartlemgvv  28293  probun  28336  ballotlemfc0  28409  ballotlemfcc  28410  sgnmul  28459  signstfvneq0  28507  erdszelem8  28620  erdszelem9  28621  erdsze2lem2  28626  cnpcon  28653  txpcon  28655  ptpcon  28656  indispcon  28657  conpcon  28658  cvxpcon  28665  cnllyscon  28668  cvmcov2  28698  cvmopnlem  28701  cvmliftmolem1  28704  cvmliftlem14  28720  cvmliftlem15  28721  cvmlift2lem13  28738  cvmlift3lem2  28743  cvmlift3lem9  28750  poseq  29309  sltres  29400  nodense  29425  nocvxmin  29427  nobndup  29436  nobnddown  29437  seglerflx  29738  seglemin  29739  btwnsegle  29743  hilbert1.1  29780  wl-2sb6d  29984  tan2h  30023  heicant  30025  mblfinlem2  30028  itg2addnc  30045  ftc2nc  30075  dvasin  30079  neibastop2lem  30154  sdclem1  30212  fdc  30214  istotbnd3  30243  sstotbnd  30247  prdstotbnd  30266  prdsbnd2  30267  cntotbnd  30268  rngoisocnv  30360  mzpcompact2lem  30660  diophrw  30668  rexrabdioph  30703  eldioph4b  30721  pellexlem5  30745  pellfund14  30810  acongtr  30892  fnwe2lem3  30974  gicabl  31023  hbtlem2  31049  hbtlem4  31051  hbtlem5  31053  dgraalem  31070  aaitgo  31087  ioounsn  31153  isprm7  31168  islptre  31579  limclner  31611  icccncfext  31644  stoweidlem1  31737  stoweidlem14  31750  stoweidlem24  31760  stoweidlem46  31782  stoweidlem57  31793  dirkercncflem2  31840  fourierdlem20  31863  fourierdlem41  31884  fourierdlem46  31889  fourierdlem48  31891  fourierdlem50  31893  fourierdlem62  31905  fourierdlem63  31906  fourierdlem64  31907  fourierdlem65  31908  fourierdlem76  31919  fourierdlem79  31922  fourierdlem103  31946  fourierdlem104  31947  raaan2  32134  mgmpropd  32417  lidlmmgm  32558  gsumlsscl  32846  lincsumcl  32902  lincscmcl  32903  isldepslvec2  32956  bj-flbi3  34483  bj-finsumval0  34538  lsmsat  34608  islfld  34662  ps-2  35077  lplnexllnN  35163  4atlem9  35202  4atlem10a  35203  lnatexN  35378  2lnat  35383  pmapjat1  35452  lhpj1  35621  lhpm0atN  35628  4atexlemex2  35670  4atex  35675  4atex2-0aOLDN  35677  4atex2-0cOLDN  35679  lautcnvle  35688  lautj  35692  lautm  35693  idltrn  35749  cdleme01N  35821  cdleme0ex1N  35823  cdleme5  35840  cdleme9  35853  cdleme11c  35861  cdleme11g  35865  cdlemefrs29bpre0  35997  cdlemefrs29cpre1  35999  cdlemefrs32fva1  36002  cdleme32fva  36038  cdleme32fva1  36039  cdleme32fvaw  36040  cdleme32d  36045  cdleme32f  36047  cdleme35fnpq  36050  cdleme48d  36136  cdleme48gfv  36138  cdleme50ltrn  36158  trlord  36170  cdlemg4b1  36210  cdlemg4b2  36211  cdlemg13a  36252  cdlemg17a  36262  cdlemg17f  36267  erng1lem  36588  erngdvlem3  36591  erngdvlem4  36592  erng1r  36596  erngdvlem3-rN  36599  erngdvlem4-rN  36600  dva0g  36629  dialss  36648  dia0  36654  dia1N  36655  diaglbN  36657  diameetN  36658  diainN  36659  diaintclN  36660  dia1dim  36663  dia2dimlem5  36670  dia2dimlem7  36672  dia2dimlem9  36674  dia2dimlem10  36675  dia2dimlem12  36677  dia2dimlem13  36678  dvhopvadd  36695  dvhvaddass  36699  dvhopvsca  36704  tendolinv  36707  tendorinv  36708  dvhlveclem  36710  dvh0g  36713  dvheveccl  36714  dvhopN  36718  docaclN  36726  diaocN  36727  djajN  36739  dib0  36766  dib1dim  36767  dibglbN  36768  dibintclN  36769  dib1dim2  36770  diblss  36772  diblsmopel  36773  dicvaddcl  36792  dicvscacl  36793  diclspsn  36796  cdlemn4a  36801  cdlemn11c  36811  dihjustlem  36818  dihord1  36820  dihord2a  36821  dihord2b  36822  dihord2cN  36823  dihord11b  36824  dihord11c  36826  dihord2pre  36827  dihlsscpre  36836  dih1dimb  36842  dib2dim  36845  dih2dimb  36846  dih2dimbALTN  36847  dihvalcq2  36849  dihopelvalcpre  36850  dihord6apre  36858  dihord5b  36861  dihord5apre  36864  dih0  36882  dihmeetlem1N  36892  dihglblem5apreN  36893  dihglblem3N  36897  dihmeetlem2N  36901  dihglbcpreN  36902  dihmeetlem4preN  36908  dih1dimatlem0  36930  dih1dimatlem  36931  dihatlat  36936  dihatexv  36940  dihglb2  36944  dihmeet  36945  dihintcl  36946  dihmeet2  36948  doch2val2  36966  dochocss  36968  dihoml4c  36978  dochdmj1  36992  djhlj  37003  djhljjN  37004  djhjlj  37005  dihsumssj  37010  djhexmid  37013  djhlsmcl  37016  djhcvat42  37017  dihjatcclem4  37023  dihjat1lem  37030  dihsmsprn  37032  dihjat3  37034  dvh3dim2  37050  dvh3dim3N  37051  dochkr1OLDN  37081  lclkrlem2c  37111  lclkrlem2d  37112  mapdpglem23  37296  hdmap11lem2  37447
  Copyright terms: Public domain W3C validator