MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl12anc Structured version   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  3735  raaanv  3736  onminex  4787  soltmin  5273  cocan1  6024  fliftfun  6034  soisores  6047  soisoi  6048  isopolem  6065  f1oiso2  6072  weniso  6075  caovcld  6240  caovcomd  6243  tfrlem12  6650  omeulem1  6825  oaabs2  6888  omabs  6890  erov  7001  frfi  7352  finsschain  7413  suplub2  7466  supmax  7470  supisolem  7475  ordiso2  7484  ordtypelem7  7493  wemaplem2  7516  wemapso2lem  7519  cantnflt  7627  cantnfp1lem3  7636  cantnflem1b  7642  cantnflem1  7645  wemapwe  7654  cnfcomlem  7656  cnfcom  7657  cnfcom3lem  7660  infxpenlem  7895  fseqenlem1  7905  dfac12lem2  8024  infpssrlem4  8186  enfin2i  8201  isf34lem7  8259  isf34lem6  8260  fin1a2lem7  8286  fin1a2lem10  8289  fin1a2lem11  8290  fin1a2lem13  8292  ttukeylem6  8394  ttukeylem7  8395  iundom2g  8415  fpwwe2lem6  8510  fpwwe2lem7  8511  fpwwe2lem9  8513  fpwwe2lem12  8516  fpwwe2  8518  canthnumlem  8523  canthwelem  8525  canthp1lem2  8528  pwfseqlem4  8537  inar1  8650  intgru  8689  distrlem4pr  8903  conjmul  9731  lediv12a  9903  recp1lt1  9908  cju  9996  gtndiv  10347  zsupss  10565  uzsupss  10568  icc0  10964  iccssioo2  10983  fzrev3  11111  fldiv  11241  modabs  11274  seqcaopr  11360  seqf1olem1  11362  seqof2  11381  crreczi  11504  hashtpg  11691  seqcoll  11712  seqcoll2  11713  sqrlem2  12049  resqrex  12056  abs1m  12139  isercoll  12461  zsum  12512  fsum2dlem  12554  fsumcom2  12558  efsub  12701  bitsinv2  12955  sqgcd  13058  qredeu  13107  pcpremul  13217  pceulem  13219  pczpre  13221  pcdiv  13226  pcqmul  13227  pcqdiv  13231  pcexp  13233  pcdvdsb  13242  pcneg  13247  pcdvdstr  13249  pcgcd1  13250  pc2dvds  13252  pcz  13254  pcaddlem  13257  pcadd  13258  qexpz  13270  expnprm  13271  infpnlem2  13279  ramub2  13382  ramub1lem1  13394  f1ocpbllem  13749  f1ovscpbl  13751  mreexexlem3d  13871  mreexexlem4d  13872  fthi  14115  ipodrsima  14591  mndpropd  14721  grpsubpropd2  14890  ghmf1  15034  odf1  15198  lsmpropd  15309  dprdf1o  15590  pgpfac1lem3  15635  pgpfac1lem5  15637  pgpfaclem1  15639  ablfaclem2  15644  rngpropd  15695  lmodprop2d  16006  lsspropd  16093  lmhmpropd  16145  lbspropd  16171  lbsextlem3  16232  lidlsubcl  16287  assapropd  16386  mplind  16562  psrplusgpropd  16629  ply1scln0  16682  iporthcom  16866  obslbs  16957  pptbas  17072  elcls  17137  neiint  17168  neiptopnei  17196  restbas  17222  neitr  17244  iscnp4  17327  cnconst2  17347  cnpdis  17357  cnt0  17410  cnhaus  17418  cmpcovf  17454  hauscmplem  17469  concompid  17494  2ndci  17511  2ndc1stc  17514  1stcrest  17516  2ndcctbss  17518  2ndcomap  17521  2ndcsep  17522  dis2ndc  17523  restlly  17546  islly2  17547  lly1stc  17559  dislly  17560  llycmpkgen2  17582  ptbasfi  17613  neitx  17639  ptpjopn  17644  ptcnplem  17653  upxp  17655  txlly  17668  txtube  17672  tx1stc  17682  txkgen  17684  xkococnlem  17691  kqreglem1  17773  kqreglem2  17774  kqnrmlem1  17775  kqnrmlem2  17776  hmeoimaf1o  17802  reghmph  17825  nrmhmph  17826  ordthmeolem  17833  trfil2  17919  fmfnfm  17990  hauspwpwf1  18019  fclsfnflim  18059  cnextf  18097  cnextcn  18098  tmdgsum2  18126  symgtgp  18131  subgntr  18136  opnsubg  18137  ghmcnp  18144  divstgpopn  18149  tsmsf1o  18174  tsmsxplem1  18182  tsmsxplem2  18183  tsmsxp  18184  ustexsym  18245  restutop  18267  imasdsf1olem  18403  blssexps  18456  blssex  18457  ssblex  18458  imasf1oxms  18519  blcld  18535  stdbdmopn  18548  met1stc  18551  met2ndci  18552  prdsxmslem2  18559  metcnp3  18570  cfilucfilOLD  18599  cfilucfil  18600  ngptgp  18677  tgioo  18827  tgqioo  18831  zdis  18847  iccpnfhmeo  18970  xrhmeo  18971  cnheibor  18980  elpi1i  19071  cmetcuspOLD  19307  pjthlem2  19339  ivthlem2  19349  ovolicc1  19412  ovolicc2lem3  19415  ovolicc2lem4  19416  volsup  19450  volivth  19499  vitalilem3  19502  mbflimsup  19558  mbfi1fseqlem1  19607  mbfi1fseqlem3  19609  mbfi1fseqlem5  19611  limcnlp  19765  limcflf  19768  limciun  19781  dvmptfsum  19859  dvcnvlem  19860  dvcvx  19904  mpfind  19965  facth1  20087  elply2  20115  coeeq  20146  aaliou3lem8  20262  ulm2  20301  mtestbdd  20321  reeff1o  20363  dcubic2  20684  quart  20701  xrlimcnp  20807  amgm  20829  harmonicbnd4  20849  perfect  21015  dchrptlem1  21048  bposlem2  21069  lgsfcl2  21086  lgsdir  21114  lgsdi  21116  lgsne0  21117  dchrvmasumlem2  21192  chpdifbndlem2  21248  pntpbnd1  21280  pntpbnd2  21281  padicabv  21324  nbgraf1olem5  21455  subgoid  21895  subgoinv  21896  ghgrp  21956  nvpi  22155  nmlno0lem  22294  fh1  23120  fh2  23121  eigposi  23339  nmlnop0iALT  23498  nmopun  23517  branmfn  23608  opsqrlem1  23643  opsqrlem6  23648  mdslmd1lem1  23828  csmdsymi  23837  atom1d  23856  chirredlem2  23894  cdj1i  23936  cdj3i  23944  ofldsqr  24240  metideq  24288  metider  24289  pstmfval  24291  lmxrge0  24337  qqhval2  24366  qqhf  24370  qqhghm  24372  qqhrhm  24373  esumpcvgval  24468  sigainb  24519  insiga  24520  imambfm  24612  dya2icoseg  24627  dya2iocnrect  24631  sibfof  24654  probun  24677  ballotlemfc0  24750  ballotlemfcc  24751  erdszelem8  24884  erdszelem9  24885  erdsze2lem2  24890  cnpcon  24917  txpcon  24919  ptpcon  24920  indispcon  24921  conpcon  24922  cvxpcon  24929  cnllyscon  24932  cvmcov2  24962  cvmopnlem  24965  cvmliftmolem1  24968  cvmliftlem14  24984  cvmliftlem15  24985  cvmlift2lem13  25002  cvmlift3lem2  25007  cvmlift3lem9  25014  fprod2dlem  25304  fprodcom2  25308  poseq  25528  sltres  25619  nodense  25644  nocvxmin  25646  nobndup  25655  nobnddown  25656  axcgrrflx  25853  axsegconlem1  25856  axcontlem2  25904  axcontlem12  25914  seglerflx  26046  seglemin  26047  btwnsegle  26051  hilbert1.1  26088  mblfinlem2  26244  itg2addnc  26259  ftc2nc  26289  finlocfin  26379  locfindis  26385  neibastop2lem  26389  sdclem1  26447  fdc  26449  istotbnd3  26480  sstotbnd  26484  prdstotbnd  26503  prdsbnd2  26504  cntotbnd  26505  rngoisocnv  26597  mzpcompact2lem  26808  diophrw  26817  rexrabdioph  26854  eldioph4b  26872  pellexlem5  26896  pellfund14  26961  acongtr  27043  fnwe2lem3  27127  gicabl  27240  hbtlem2  27305  hbtlem4  27307  hbtlem5  27309  dgraalem  27327  aaitgo  27344  f1omvdmvd  27363  f1otrspeq  27367  psgnunilem2  27395  psgnunilem3  27396  psgnvalii  27409  stoweidlem1  27726  stoweidlem14  27739  stoweidlem24  27749  stoweidlem46  27771  stoweidlem57  27782  raaan2  27929  modifeq2int  28161  wrdlenge2n0  28176  swrdccat3b  28219  swrdtrcfvl  28265  2spotiundisj  28451  lsmsat  29806  islfld  29860  ps-2  30275  lplnexllnN  30361  4atlem9  30400  4atlem10a  30401  lnatexN  30576  2lnat  30581  pmapjat1  30650  lhpj1  30819  lhpm0atN  30826  4atexlemex2  30868  4atex  30873  4atex2-0aOLDN  30875  4atex2-0cOLDN  30877  lautcnvle  30886  lautj  30890  lautm  30891  idltrn  30947  cdleme01N  31018  cdleme0ex1N  31020  cdleme5  31037  cdleme9  31050  cdleme11c  31058  cdleme11g  31062  cdlemefrs29bpre0  31193  cdlemefrs29cpre1  31195  cdlemefrs32fva1  31198  cdleme32fva  31234  cdleme32fva1  31235  cdleme32fvaw  31236  cdleme32d  31241  cdleme32f  31243  cdleme35fnpq  31246  cdleme48d  31332  cdleme48gfv  31334  cdleme50ltrn  31354  trlord  31366  cdlemg4b1  31406  cdlemg4b2  31407  cdlemg13a  31448  cdlemg17a  31458  cdlemg17f  31463  erng1lem  31784  erngdvlem3  31787  erngdvlem4  31788  erng1r  31792  erngdvlem3-rN  31795  erngdvlem4-rN  31796  dva0g  31825  dialss  31844  dia0  31850  dia1N  31851  diaglbN  31853  diameetN  31854  diainN  31855  diaintclN  31856  dia1dim  31859  dia2dimlem5  31866  dia2dimlem7  31868  dia2dimlem9  31870  dia2dimlem10  31871  dia2dimlem12  31873  dia2dimlem13  31874  dvhopvadd  31891  dvhvaddass  31895  dvhopvsca  31900  tendolinv  31903  tendorinv  31904  dvhlveclem  31906  dvh0g  31909  dvheveccl  31910  dvhopN  31914  docaclN  31922  diaocN  31923  djajN  31935  dib0  31962  dib1dim  31963  dibglbN  31964  dibintclN  31965  dib1dim2  31966  diblss  31968  diblsmopel  31969  dicvaddcl  31988  dicvscacl  31989  diclspsn  31992  cdlemn4a  31997  cdlemn11c  32007  dihjustlem  32014  dihord1  32016  dihord2a  32017  dihord2b  32018  dihord2cN  32019  dihord11b  32020  dihord11c  32022  dihord2pre  32023  dihlsscpre  32032  dih1dimb  32038  dib2dim  32041  dih2dimb  32042  dih2dimbALTN  32043  dihvalcq2  32045  dihopelvalcpre  32046  dihord6apre  32054  dihord5b  32057  dihord5apre  32060  dih0  32078  dihmeetlem1N  32088  dihglblem5apreN  32089  dihglblem3N  32093  dihmeetlem2N  32097  dihglbcpreN  32098  dihmeetlem4preN  32104  dih1dimatlem0  32126  dih1dimatlem  32127  dihatlat  32132  dihatexv  32136  dihglb2  32140  dihmeet  32141  dihintcl  32142  dihmeet2  32144  doch2val2  32162  dochocss  32164  dihoml4c  32174  dochdmj1  32188  djhlj  32199  djhljjN  32200  djhjlj  32201  dihsumssj  32206  djhexmid  32209  djhlsmcl  32212  djhcvat42  32213  dihjatcclem4  32219  dihjat1lem  32226  dihsmsprn  32228  dihjat3  32230  dvh3dim2  32246  dvh3dim3N  32247  dochkr1OLDN  32277  lclkrlem2c  32307  lclkrlem2d  32308  mapdpglem23  32492  hdmap11lem2  32643
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