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

Theorem syl12anc 1180
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 521 . 2  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
5 syl12anc.4 . 2  |-  ( ( ps  /\  ( ch 
/\  th ) )  ->  ta )
64, 5syl 15 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  syl22anc  1183  raaan  3561  raaanv  3562  onminex  4598  soltmin  5082  cocan1  5801  fliftfun  5811  soisores  5824  soisoi  5825  isopolem  5842  f1oiso2  5849  weniso  5852  caovcld  6013  caovcomd  6016  tfrlem12  6405  omeulem1  6580  oaabs2  6643  omabs  6645  erov  6755  frfi  7102  finsschain  7162  suplub2  7212  supmax  7216  supisolem  7221  ordiso2  7230  ordtypelem7  7239  wemaplem2  7262  wemapso2lem  7265  cantnflt  7373  cantnfp1lem3  7382  cantnflem1b  7388  cantnflem1  7391  wemapwe  7400  cnfcomlem  7402  cnfcom  7403  cnfcom3lem  7406  infxpenlem  7641  fseqenlem1  7651  dfac12lem2  7770  infpssrlem4  7932  enfin2i  7947  isf34lem7  8005  isf34lem6  8006  fin1a2lem7  8032  fin1a2lem10  8035  fin1a2lem11  8036  fin1a2lem13  8038  ttukeylem6  8141  ttukeylem7  8142  iundom2g  8162  fpwwe2lem6  8257  fpwwe2lem7  8258  fpwwe2lem9  8260  fpwwe2lem12  8263  fpwwe2  8265  canthnumlem  8270  canthwelem  8272  canthp1lem2  8275  pwfseqlem4  8284  inar1  8397  intgru  8436  distrlem4pr  8650  conjmul  9477  lediv12a  9649  recp1lt1  9654  lbinfm  9707  cju  9742  gtndiv  10089  zsupss  10307  uzsupss  10310  icc0  10704  iccssioo2  10722  fzrev3  10849  fldiv  10964  modabs  10997  seqcaopr  11083  seqf1olem1  11085  crreczi  11226  seqcoll  11401  seqcoll2  11402  sqrlem2  11729  resqrex  11736  abs1m  11819  isercoll  12141  zsum  12191  fsum2dlem  12233  fsumcom2  12237  efsub  12380  bitsinv2  12634  sqgcd  12737  qredeu  12786  pcpremul  12896  pceulem  12898  pczpre  12900  pcdiv  12905  pcqmul  12906  pcqdiv  12910  pcexp  12912  pcdvdsb  12921  pcneg  12926  pcdvdstr  12928  pcgcd1  12929  pc2dvds  12931  pcz  12933  pcaddlem  12936  pcadd  12937  qexpz  12949  expnprm  12950  infpnlem2  12958  ramub2  13061  ramub1lem1  13073  f1ocpbllem  13426  f1ovscpbl  13428  mreexexlem3d  13548  mreexexlem4d  13549  fthi  13792  ipodrsima  14268  mndpropd  14398  grpsubpropd2  14567  ghmf1  14711  odf1  14875  lsmpropd  14986  dprdf1o  15267  pgpfac1lem3  15312  pgpfac1lem5  15314  pgpfaclem1  15316  ablfaclem2  15321  rngpropd  15372  lmodprop2d  15687  lsspropd  15774  lmhmpropd  15826  lbspropd  15852  lbsextlem3  15913  lidlsubcl  15968  assapropd  16067  mplind  16243  psrplusgpropd  16313  ply1scln0  16366  iporthcom  16539  obslbs  16630  pptbas  16745  elcls  16810  neiint  16841  restbas  16889  cnconst2  17011  cnpdis  17021  cnt0  17074  cnhaus  17082  cmpcovf  17118  hauscmplem  17133  concompid  17157  2ndci  17174  2ndc1stc  17177  1stcrest  17179  2ndcctbss  17181  2ndcomap  17184  2ndcsep  17185  dis2ndc  17186  restlly  17209  islly2  17210  lly1stc  17222  dislly  17223  llycmpkgen2  17245  ptbasfi  17276  ptpjopn  17306  ptcnplem  17315  upxp  17317  txlly  17330  txtube  17334  tx1stc  17344  txkgen  17346  xkococnlem  17353  kqreglem1  17432  kqreglem2  17433  kqnrmlem1  17434  kqnrmlem2  17435  hmeoimaf1o  17461  reghmph  17484  nrmhmph  17485  ordthmeolem  17492  trfil2  17582  fmfnfm  17653  hauspwpwf1  17682  fclsfnflim  17722  tmdgsum2  17779  symgtgp  17784  subgntr  17789  opnsubg  17790  ghmcnp  17797  divstgpopn  17802  tsmsf1o  17827  tsmsxplem1  17835  tsmsxplem2  17836  tsmsxp  17837  imasdsf1olem  17937  blssex  17973  ssblex  17974  imasf1oxms  18035  blcld  18051  stdbdmopn  18064  met1stc  18067  met2ndci  18068  prdsxmslem2  18075  metcnp3  18086  ngptgp  18152  tgioo  18302  tgqioo  18306  zdis  18322  iccpnfhmeo  18443  xrhmeo  18444  cnheibor  18453  elpi1i  18544  pjthlem2  18802  ivthlem2  18812  ovolicc1  18875  ovolicc2lem3  18878  ovolicc2lem4  18879  volsup  18913  volivth  18962  vitalilem3  18965  mbflimsup  19021  mbfi1fseqlem1  19070  mbfi1fseqlem3  19072  mbfi1fseqlem5  19074  limcnlp  19228  limcflf  19231  limciun  19244  dvmptfsum  19322  dvcnvlem  19323  dvcvx  19367  mpfind  19428  facth1  19550  elply2  19578  coeeq  19609  aaliou3lem8  19725  ulm2  19764  reeff1o  19823  dcubic2  20140  quart  20157  xrlimcnp  20263  amgm  20285  harmonicbnd4  20304  perfect  20470  dchrptlem1  20503  bposlem2  20524  lgsfcl2  20541  lgsdir  20569  lgsdi  20571  lgsne0  20572  dchrvmasumlem2  20647  chpdifbndlem2  20703  pntpbnd1  20735  pntpbnd2  20736  padicabv  20779  subgoid  20974  subgoinv  20975  ghgrp  21035  nvpi  21232  nmlno0lem  21371  fh1  22197  fh2  22198  eigposi  22416  nmlnop0iALT  22575  nmopun  22594  branmfn  22685  opsqrlem1  22720  opsqrlem6  22725  mdslmd1lem1  22905  csmdsymi  22914  atom1d  22933  chirredlem2  22971  cdj1i  23013  cdj3i  23021  ifeqeqx  23034  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemsdom  23070  lmxrge0  23375  esumpcvgval  23446  sigainb  23497  insiga  23498  imambfm  23567  erdszelem8  23729  erdszelem9  23730  erdsze2lem2  23735  cnpcon  23761  txpcon  23763  ptpcon  23764  indispcon  23765  conpcon  23766  cvxpcon  23773  cnllyscon  23776  cvmcov2  23806  cvmopnlem  23809  cvmliftmolem1  23812  cvmliftlem14  23828  cvmliftlem15  23829  cvmlift2lem13  23846  cvmlift3lem2  23851  cvmlift3lem9  23858  poseq  24253  sltres  24318  nodense  24343  nocvxmin  24345  nobndup  24354  nobnddown  24355  axcgrrflx  24542  axsegconlem1  24545  axcontlem2  24593  axcontlem12  24603  seglerflx  24735  seglemin  24736  btwnsegle  24740  hilbert1.1  24777  dblsubvec  25474  mvecrtol2  25477  mulinvsca  25480  iscnp4  25563  prdnei  25573  islimrs4  25582  indcls2  25996  pxysxy  26142  finlocfin  26299  locfindis  26305  neibastop2lem  26309  sdclem1  26453  fdc  26455  istotbnd3  26495  sstotbnd  26499  prdstotbnd  26518  prdsbnd2  26519  cntotbnd  26520  rngoisocnv  26612  mzpcompact2lem  26829  diophrw  26838  rexrabdioph  26875  eldioph4b  26894  pellexlem5  26918  pellfund14  26983  acongtr  27065  fnwe2lem3  27149  gicabl  27263  hbtlem2  27328  hbtlem4  27330  hbtlem5  27332  dgraalem  27350  aaitgo  27367  f1omvdmvd  27386  f1otrspeq  27390  psgnunilem2  27418  psgnunilem3  27419  psgnvalii  27432  raaan2  27953  lsmsat  29198  islfld  29252  ps-2  29667  lplnexllnN  29753  4atlem9  29792  4atlem10a  29793  lnatexN  29968  2lnat  29973  pmapjat1  30042  lhpj1  30211  lhpm0atN  30218  4atexlemex2  30260  4atex  30265  4atex2-0aOLDN  30267  4atex2-0cOLDN  30269  lautcnvle  30278  lautj  30282  lautm  30283  idltrn  30339  cdleme01N  30410  cdleme0ex1N  30412  cdleme5  30429  cdleme9  30442  cdleme11c  30450  cdleme11g  30454  cdlemefrs29bpre0  30585  cdlemefrs29cpre1  30587  cdlemefrs32fva1  30590  cdleme32fva  30626  cdleme32fva1  30627  cdleme32fvaw  30628  cdleme32d  30633  cdleme32f  30635  cdleme35fnpq  30638  cdleme48d  30724  cdleme48gfv  30726  cdleme50ltrn  30746  trlord  30758  cdlemg4b1  30798  cdlemg4b2  30799  cdlemg13a  30840  cdlemg17a  30850  cdlemg17f  30855  erng1lem  31176  erngdvlem3  31179  erngdvlem4  31180  erng1r  31184  erngdvlem3-rN  31187  erngdvlem4-rN  31188  dva0g  31217  dialss  31236  dia0  31242  dia1N  31243  diaglbN  31245  diameetN  31246  diainN  31247  diaintclN  31248  dia1dim  31251  dia2dimlem5  31258  dia2dimlem7  31260  dia2dimlem9  31262  dia2dimlem10  31263  dia2dimlem12  31265  dia2dimlem13  31266  dvhopvadd  31283  dvhvaddass  31287  dvhopvsca  31292  tendolinv  31295  tendorinv  31296  dvhlveclem  31298  dvh0g  31301  dvheveccl  31302  dvhopN  31306  docaclN  31314  diaocN  31315  djajN  31327  dib0  31354  dib1dim  31355  dibglbN  31356  dibintclN  31357  dib1dim2  31358  diblss  31360  diblsmopel  31361  dicvaddcl  31380  dicvscacl  31381  diclspsn  31384  cdlemn4a  31389  cdlemn11c  31399  dihjustlem  31406  dihord1  31408  dihord2a  31409  dihord2b  31410  dihord2cN  31411  dihord11b  31412  dihord11c  31414  dihord2pre  31415  dihlsscpre  31424  dih1dimb  31430  dib2dim  31433  dih2dimb  31434  dih2dimbALTN  31435  dihvalcq2  31437  dihopelvalcpre  31438  dihord6apre  31446  dihord5b  31449  dihord5apre  31452  dih0  31470  dihmeetlem1N  31480  dihglblem5apreN  31481  dihglblem3N  31485  dihmeetlem2N  31489  dihglbcpreN  31490  dihmeetlem4preN  31496  dih1dimatlem0  31518  dih1dimatlem  31519  dihatlat  31524  dihatexv  31528  dihglb2  31532  dihmeet  31533  dihintcl  31534  dihmeet2  31536  doch2val2  31554  dochocss  31556  dihoml4c  31566  dochdmj1  31580  djhlj  31591  djhljjN  31592  djhjlj  31593  dihsumssj  31598  djhexmid  31601  djhlsmcl  31604  djhcvat42  31605  dihjatcclem4  31611  dihjat1lem  31618  dihsmsprn  31620  dihjat3  31622  dvh3dim2  31638  dvh3dim3N  31639  dochkr1OLDN  31669  lclkrlem2c  31699  lclkrlem2d  31700  mapdpglem23  31884  hdmap11lem2  32035
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator