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

Theorem sylan2b 462
Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)
Hypotheses
Ref Expression
sylan2b.1  |-  ( ph  <->  ch )
sylan2b.2  |-  ( ( ps  /\  ch )  ->  th )
Assertion
Ref Expression
sylan2b  |-  ( ( ps  /\  ph )  ->  th )

Proof of Theorem sylan2b
StepHypRef Expression
1 sylan2b.1 . . 3  |-  ( ph  <->  ch )
21biimpi 187 . 2  |-  ( ph  ->  ch )
3 sylan2b.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan2 461 1  |-  ( ( ps  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  syl2anb  466  bm1.1  2373  eqtr3  2407  morex  3062  psssstr  3397  reuss2  3565  reupick  3569  reximdva0  3583  rabsneu  3823  opabss  4211  triun  4257  poirr  4456  wefrc  4518  ordsucuniel  4745  onzsl  4767  xpcan  5246  soex  5260  fnfco  5550  fun11iun  5636  suppssr  5804  eldmrexrnb  5817  fnressn  5858  fvtp3  5881  fvtp3g  5884  f1mpt  5947  offval  6252  dfoprab3  6343  1stconst  6375  2ndconst  6376  poxp  6395  fnwelem  6398  tfrlem2  6574  oeordsuc  6774  oelim2  6775  omsmolem  6833  fisucdomOLD  7249  ssnnfi  7265  fiint  7320  unifi  7332  indexfi  7350  iinfi  7358  unwdomg  7486  inf3lem5  7521  rankr1bg  7663  rankr1c  7681  carden2a  7787  dfac8clem  7847  dfac5lem4  7941  pwsdompw  8018  cfsuc  8071  cflim2  8077  enfin2i  8135  isf34lem4  8191  axdc4lem  8269  zornn0g  8319  uniimadomf  8354  fpwwe2lem8  8446  fpwwe2lem12  8450  fpwwe2lem13  8451  pwfseqlem1  8467  pwfseqlem5  8472  intgru  8623  addclpi  8703  addnidpi  8712  ltsonq  8780  nqpr  8825  reclem3pr  8860  recexsr  8916  supsrlem  8920  infmrcl  9920  nnnn0addcl  10184  un0addcl  10186  un0mulcl  10187  uzind3  10296  uzind3OLD  10298  uzind4  10467  zsupss  10498  rpnnen1lem1  10533  rpnnen1lem2  10534  rpnnen1lem3  10535  rpnnen1lem5  10537  ltsubrp  10576  ltaddrp  10577  xrlttr  10666  qbtwnxr  10719  xltnegi  10735  xaddnemnf  10753  xaddnepnf  10754  xaddcom  10757  xnegdi  10760  xsubge0  10773  xrub  10823  fzind2  11126  seqof  11308  expp1  11316  expneg  11317  expcllem  11320  mulexpz  11348  expaddz  11352  expmulz  11354  faclbnd4lem3  11514  faclbnd4  11516  brfi1uzind  11643  swrd00  11693  cats1un  11718  shftf  11822  sqrdiv  11999  leabs  12032  mulcn2  12317  summolem2  12438  fsumrev2  12493  geomulcvg  12581  ruclem6  12762  dvdseq  12825  dvdsfac  12832  gcdcllem1  12939  rpexp1i  13049  hashdvds  13092  iserodd  13137  pcqcl  13158  pcid  13174  ismred  13755  funcpropd  14025  natpropd  14101  latlem12  14435  clatl  14471  lubun  14478  odupos  14490  grpinvnzcl  14791  mulgneg  14836  mulgnn0z  14838  pgpssslw  15176  sylow2alem2  15180  sylow2a  15181  oddvdssubg  15398  gsumunsn  15472  gsum2d  15474  ablfac1eu  15559  pgpfac1lem5  15565  gsumdixp  15643  dvdsrcl2  15683  isdrngd  15788  evlslem4  16492  coe1tmmul2  16596  cnsubrg  16683  intcld  17028  neiptopnei  17120  ordtrest2lem  17190  lmss  17285  cmpcovf  17377  cncmp  17378  fincmp  17379  cmpsublem  17385  cmpsub  17386  uncon  17414  1stcfb  17430  2ndcsep  17444  1stckgenlem  17507  ptbasin  17531  ptbasfi  17535  ptunimpt  17549  ptuniconst  17552  dfac14  17572  ptcnp  17576  xkoptsub  17608  xkococnlem  17613  xkoinjcn  17641  qtopcmplem  17661  qtophmeo  17771  fbfinnfr  17795  isfcls  17963  xmetrtri  18294  xmetrtri2  18295  blssioo  18698  divcn  18770  bndth  18855  resscdrg  19180  minveclem3  19198  finiunmbl  19306  opnmbllem  19361  ismbf2d  19401  itg2seq  19502  ellimc2  19632  limcmpt2  19639  limcres  19641  dvlem  19651  dvidlem  19670  dvrec  19709  dveflem  19731  dvlip  19745  coe1mul3  19890  dvtaylp  20154  leibpilem2  20649  leibpi  20650  wilthlem2  20720  basellem3  20733  dvdsflip  20835  dchreq  20910  dchrsum  20921  lgsval3  20966  lgsdir2lem4  20978  2sqlem6  21021  rpvmasumlem  21049  dchrisum0fno1  21073  rpvmasum2  21074  pntrsumbnd2  21129  ostthlem1  21189  umgraex  21226  usgraidx2vlem1  21277  nbgraf1olem3  21320  nbgraf1olem5  21322  cusconngra  21512  grpoidinvlem3  21643  ablo32  21723  ablomuldiv  21726  ablodivdiv  21727  ablodiv32  21729  nvadd12  21951  nvscom  21959  nvsubsub23  21992  dipassr  22196  htthlem  22269  hsn0elch  22599  shscli  22668  nmopun  23366  branmfn  23457  mdslj1i  23671  mdslj2i  23672  atss  23698  chcv1  23707  dmdbr5ati  23774  isoun  23931  esumsplit  24244  esumpcvgval  24265  sigaclcu2  24300  volmeas  24382  mbfmco2  24410  ballotlemfc0  24530  ballotlemfcc  24531  subfacp1lem4  24649  erdszelem7  24663  erdszelem8  24664  erdsze2lem2  24670  rescon  24713  cvmsdisj  24737  cvmscld  24740  climuzcnv  24888  prodmolem2  25041  zprod  25043  prodsn  25066  trpredmintr  25259  axcontlem2  25619  axcontlem7  25624  cgrid2  25652  btwncom  25663  btwnswapid2  25667  colinearperm1  25711  colinearperm3  25712  colinearperm2  25713  colinearperm4  25714  lineext  25725  colinbtwnle  25767  broutsideof2  25771  outsideofcom  25777  linecom  25799  linerflx2  25800  lineintmo  25806  bpolydiflem  25815  bpoly2  25818  bpoly3  25819  hfext  25839  bddiblnc  25976  ntruni  26022  clsint2  26024  locfincmp  26076  neibastop1  26080  eqfnun  26115  ac6gf  26126  heibor1lem  26210  isdrngo2  26266  unichnidl  26333  isfldidl  26370  ismrcd1  26444  isnacs3  26456  pellfundglb  26640  jm2.22  26758  jm2.23  26759  isnumbasgrplem1  26936  hbtlem6  27003  rngunsnply  27048  issubmd  27053  symgsssg  27078  symgfisg  27079  gsumcom3  27124  hashgcdlem  27186  phisum  27188  afv0nbfvbi  27685  bnj521  28443  bnj926  28477  bnj1109  28496  bnj1294  28528  bnj545  28605  bnj605  28617  bnj594  28622  bnj934  28645  bnj953  28649  bnj1137  28703  bnj1174  28711  bnj1388  28741  lubunNEW  29089  lkrss2N  29285  elpadd0  29924  ltrnu  30236  tendoex  31090  cdlemm10N  31234  dicfnN  31299  dihmeetlem2N  31415  dihlatat  31453  lcfrlem9  31666
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