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

Theorem syl12anc 1182
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 522 . 2  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
5 syl12anc.4 . 2  |-  ( ( ps  /\  ( ch 
/\  th ) )  ->  ta )
64, 5syl 16 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  syl22anc  1185  raaan  3695  raaanv  3696  onminex  4746  soltmin  5232  cocan1  5983  fliftfun  5993  soisores  6006  soisoi  6007  isopolem  6024  f1oiso2  6031  weniso  6034  caovcld  6199  caovcomd  6202  tfrlem12  6609  omeulem1  6784  oaabs2  6847  omabs  6849  erov  6960  frfi  7311  finsschain  7371  suplub2  7422  supmax  7426  supisolem  7431  ordiso2  7440  ordtypelem7  7449  wemaplem2  7472  wemapso2lem  7475  cantnflt  7583  cantnfp1lem3  7592  cantnflem1b  7598  cantnflem1  7601  wemapwe  7610  cnfcomlem  7612  cnfcom  7613  cnfcom3lem  7616  infxpenlem  7851  fseqenlem1  7861  dfac12lem2  7980  infpssrlem4  8142  enfin2i  8157  isf34lem7  8215  isf34lem6  8216  fin1a2lem7  8242  fin1a2lem10  8245  fin1a2lem11  8246  fin1a2lem13  8248  ttukeylem6  8350  ttukeylem7  8351  iundom2g  8371  fpwwe2lem6  8466  fpwwe2lem7  8467  fpwwe2lem9  8469  fpwwe2lem12  8472  fpwwe2  8474  canthnumlem  8479  canthwelem  8481  canthp1lem2  8484  pwfseqlem4  8493  inar1  8606  intgru  8645  distrlem4pr  8859  conjmul  9687  lediv12a  9859  recp1lt1  9864  cju  9952  gtndiv  10303  zsupss  10521  uzsupss  10524  icc0  10920  iccssioo2  10939  fzrev3  11067  fldiv  11196  modabs  11229  seqcaopr  11315  seqf1olem1  11317  seqof2  11336  crreczi  11459  hashtpg  11646  seqcoll  11667  seqcoll2  11668  sqrlem2  12004  resqrex  12011  abs1m  12094  isercoll  12416  zsum  12467  fsum2dlem  12509  fsumcom2  12513  efsub  12656  bitsinv2  12910  sqgcd  13013  qredeu  13062  pcpremul  13172  pceulem  13174  pczpre  13176  pcdiv  13181  pcqmul  13182  pcqdiv  13186  pcexp  13188  pcdvdsb  13197  pcneg  13202  pcdvdstr  13204  pcgcd1  13205  pc2dvds  13207  pcz  13209  pcaddlem  13212  pcadd  13213  qexpz  13225  expnprm  13226  infpnlem2  13234  ramub2  13337  ramub1lem1  13349  f1ocpbllem  13704  f1ovscpbl  13706  mreexexlem3d  13826  mreexexlem4d  13827  fthi  14070  ipodrsima  14546  mndpropd  14676  grpsubpropd2  14845  ghmf1  14989  odf1  15153  lsmpropd  15264  dprdf1o  15545  pgpfac1lem3  15590  pgpfac1lem5  15592  pgpfaclem1  15594  ablfaclem2  15599  rngpropd  15650  lmodprop2d  15961  lsspropd  16048  lmhmpropd  16100  lbspropd  16126  lbsextlem3  16187  lidlsubcl  16242  assapropd  16341  mplind  16517  psrplusgpropd  16584  ply1scln0  16637  iporthcom  16821  obslbs  16912  pptbas  17027  elcls  17092  neiint  17123  neiptopnei  17151  restbas  17176  neitr  17198  iscnp4  17281  cnconst2  17301  cnpdis  17311  cnt0  17364  cnhaus  17372  cmpcovf  17408  hauscmplem  17423  concompid  17447  2ndci  17464  2ndc1stc  17467  1stcrest  17469  2ndcctbss  17471  2ndcomap  17474  2ndcsep  17475  dis2ndc  17476  restlly  17499  islly2  17500  lly1stc  17512  dislly  17513  llycmpkgen2  17535  ptbasfi  17566  neitx  17592  ptpjopn  17597  ptcnplem  17606  upxp  17608  txlly  17621  txtube  17625  tx1stc  17635  txkgen  17637  xkococnlem  17644  kqreglem1  17726  kqreglem2  17727  kqnrmlem1  17728  kqnrmlem2  17729  hmeoimaf1o  17755  reghmph  17778  nrmhmph  17779  ordthmeolem  17786  trfil2  17872  fmfnfm  17943  hauspwpwf1  17972  fclsfnflim  18012  cnextf  18050  cnextcn  18051  tmdgsum2  18079  symgtgp  18084  subgntr  18089  opnsubg  18090  ghmcnp  18097  divstgpopn  18102  tsmsf1o  18127  tsmsxplem1  18135  tsmsxplem2  18136  tsmsxp  18137  ustexsym  18198  restutop  18220  imasdsf1olem  18356  blssexps  18409  blssex  18410  ssblex  18411  imasf1oxms  18472  blcld  18488  stdbdmopn  18501  met1stc  18504  met2ndci  18505  prdsxmslem2  18512  metcnp3  18523  cfilucfilOLD  18552  cfilucfil  18553  ngptgp  18630  tgioo  18780  tgqioo  18784  zdis  18800  iccpnfhmeo  18923  xrhmeo  18924  cnheibor  18933  elpi1i  19024  cmetcuspOLD  19260  pjthlem2  19292  ivthlem2  19302  ovolicc1  19365  ovolicc2lem3  19368  ovolicc2lem4  19369  volsup  19403  volivth  19452  vitalilem3  19455  mbflimsup  19511  mbfi1fseqlem1  19560  mbfi1fseqlem3  19562  mbfi1fseqlem5  19564  limcnlp  19718  limcflf  19721  limciun  19734  dvmptfsum  19812  dvcnvlem  19813  dvcvx  19857  mpfind  19918  facth1  20040  elply2  20068  coeeq  20099  aaliou3lem8  20215  ulm2  20254  mtestbdd  20274  reeff1o  20316  dcubic2  20637  quart  20654  xrlimcnp  20760  amgm  20782  harmonicbnd4  20802  perfect  20968  dchrptlem1  21001  bposlem2  21022  lgsfcl2  21039  lgsdir  21067  lgsdi  21069  lgsne0  21070  dchrvmasumlem2  21145  chpdifbndlem2  21201  pntpbnd1  21233  pntpbnd2  21234  padicabv  21277  nbgraf1olem5  21408  subgoid  21848  subgoinv  21849  ghgrp  21909  nvpi  22108  nmlno0lem  22247  fh1  23073  fh2  23074  eigposi  23292  nmlnop0iALT  23451  nmopun  23470  branmfn  23561  opsqrlem1  23596  opsqrlem6  23601  mdslmd1lem1  23781  csmdsymi  23790  atom1d  23809  chirredlem2  23847  cdj1i  23889  cdj3i  23897  ofldsqr  24193  metideq  24241  metider  24242  pstmfval  24244  lmxrge0  24290  qqhval2  24319  qqhf  24323  qqhghm  24325  qqhrhm  24326  esumpcvgval  24421  sigainb  24472  insiga  24473  imambfm  24565  dya2icoseg  24580  dya2iocnrect  24584  sibfof  24607  probun  24630  ballotlemfc0  24703  ballotlemfcc  24704  erdszelem8  24837  erdszelem9  24838  erdsze2lem2  24843  cnpcon  24870  txpcon  24872  ptpcon  24873  indispcon  24874  conpcon  24875  cvxpcon  24882  cnllyscon  24885  cvmcov2  24915  cvmopnlem  24918  cvmliftmolem1  24921  cvmliftlem14  24937  cvmliftlem15  24938  cvmlift2lem13  24955  cvmlift3lem2  24960  cvmlift3lem9  24967  fprod2dlem  25257  fprodcom2  25261  poseq  25467  sltres  25532  nodense  25557  nocvxmin  25559  nobndup  25568  nobnddown  25569  axcgrrflx  25757  axsegconlem1  25760  axcontlem2  25808  axcontlem12  25818  seglerflx  25950  seglemin  25951  btwnsegle  25955  hilbert1.1  25992  mblfinlem  26143  itg2addnc  26158  finlocfin  26269  locfindis  26275  neibastop2lem  26279  sdclem1  26337  fdc  26339  istotbnd3  26370  sstotbnd  26374  prdstotbnd  26393  prdsbnd2  26394  cntotbnd  26395  rngoisocnv  26487  mzpcompact2lem  26698  diophrw  26707  rexrabdioph  26744  eldioph4b  26762  pellexlem5  26786  pellfund14  26851  acongtr  26933  fnwe2lem3  27017  gicabl  27131  hbtlem2  27196  hbtlem4  27198  hbtlem5  27200  dgraalem  27218  aaitgo  27235  f1omvdmvd  27254  f1otrspeq  27258  psgnunilem2  27286  psgnunilem3  27287  psgnvalii  27300  stoweidlem1  27617  stoweidlem14  27630  stoweidlem24  27640  stoweidlem46  27662  stoweidlem57  27673  raaan2  27820  swrdccat3b  28031  2spotiundisj  28165  lsmsat  29491  islfld  29545  ps-2  29960  lplnexllnN  30046  4atlem9  30085  4atlem10a  30086  lnatexN  30261  2lnat  30266  pmapjat1  30335  lhpj1  30504  lhpm0atN  30511  4atexlemex2  30553  4atex  30558  4atex2-0aOLDN  30560  4atex2-0cOLDN  30562  lautcnvle  30571  lautj  30575  lautm  30576  idltrn  30632  cdleme01N  30703  cdleme0ex1N  30705  cdleme5  30722  cdleme9  30735  cdleme11c  30743  cdleme11g  30747  cdlemefrs29bpre0  30878  cdlemefrs29cpre1  30880  cdlemefrs32fva1  30883  cdleme32fva  30919  cdleme32fva1  30920  cdleme32fvaw  30921  cdleme32d  30926  cdleme32f  30928  cdleme35fnpq  30931  cdleme48d  31017  cdleme48gfv  31019  cdleme50ltrn  31039  trlord  31051  cdlemg4b1  31091  cdlemg4b2  31092  cdlemg13a  31133  cdlemg17a  31143  cdlemg17f  31148  erng1lem  31469  erngdvlem3  31472  erngdvlem4  31473  erng1r  31477  erngdvlem3-rN  31480  erngdvlem4-rN  31481  dva0g  31510  dialss  31529  dia0  31535  dia1N  31536  diaglbN  31538  diameetN  31539  diainN  31540  diaintclN  31541  dia1dim  31544  dia2dimlem5  31551  dia2dimlem7  31553  dia2dimlem9  31555  dia2dimlem10  31556  dia2dimlem12  31558  dia2dimlem13  31559  dvhopvadd  31576  dvhvaddass  31580  dvhopvsca  31585  tendolinv  31588  tendorinv  31589  dvhlveclem  31591  dvh0g  31594  dvheveccl  31595  dvhopN  31599  docaclN  31607  diaocN  31608  djajN  31620  dib0  31647  dib1dim  31648  dibglbN  31649  dibintclN  31650  dib1dim2  31651  diblss  31653  diblsmopel  31654  dicvaddcl  31673  dicvscacl  31674  diclspsn  31677  cdlemn4a  31682  cdlemn11c  31692  dihjustlem  31699  dihord1  31701  dihord2a  31702  dihord2b  31703  dihord2cN  31704  dihord11b  31705  dihord11c  31707  dihord2pre  31708  dihlsscpre  31717  dih1dimb  31723  dib2dim  31726  dih2dimb  31727  dih2dimbALTN  31728  dihvalcq2  31730  dihopelvalcpre  31731  dihord6apre  31739  dihord5b  31742  dihord5apre  31745  dih0  31763  dihmeetlem1N  31773  dihglblem5apreN  31774  dihglblem3N  31778  dihmeetlem2N  31782  dihglbcpreN  31783  dihmeetlem4preN  31789  dih1dimatlem0  31811  dih1dimatlem  31812  dihatlat  31817  dihatexv  31821  dihglb2  31825  dihmeet  31826  dihintcl  31827  dihmeet2  31829  doch2val2  31847  dochocss  31849  dihoml4c  31859  dochdmj1  31873  djhlj  31884  djhljjN  31885  djhjlj  31886  dihsumssj  31891  djhexmid  31894  djhlsmcl  31897  djhcvat42  31898  dihjatcclem4  31904  dihjat1lem  31911  dihsmsprn  31913  dihjat3  31915  dvh3dim2  31931  dvh3dim3N  31932  dochkr1OLDN  31962  lclkrlem2c  31992  lclkrlem2d  31993  mapdpglem23  32177  hdmap11lem2  32328
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 178  df-an 361
  Copyright terms: Public domain W3C validator