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

Theorem sylan2b 463
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 188 . 2  |-  ( ph  ->  ch )
3 sylan2b.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan2 462 1  |-  ( ( ps  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  syl2anb  467  bm1.1  2428  eqtr3  2462  morex  3127  psssstr  3442  reuss2  3609  reupick  3613  reximdva0  3627  rabsneu  3908  opabss  4300  triun  4346  poirr  4549  wefrc  4611  ordsucuniel  4839  onzsl  4861  xpcan  5340  soex  5354  fnfco  5644  fun11iun  5730  suppssr  5900  eldmrexrnb  5913  fnressn  5954  fvtp3  5977  fvtp3g  5980  f1mpt  6043  offval  6348  dfoprab3  6439  1stconst  6471  2ndconst  6472  poxp  6494  fnwelem  6497  tfrlem2  6673  oeordsuc  6873  oelim2  6874  omsmolem  6932  fisucdomOLD  7348  ssnnfi  7364  fiint  7419  unifi  7431  indexfi  7450  iinfi  7458  unwdomg  7588  inf3lem5  7623  rankr1bg  7765  rankr1c  7783  carden2a  7891  dfac8clem  7951  dfac5lem4  8045  pwsdompw  8122  cfsuc  8175  cflim2  8181  enfin2i  8239  isf34lem4  8295  axdc4lem  8373  zornn0g  8423  uniimadomf  8458  fpwwe2lem8  8550  fpwwe2lem12  8554  fpwwe2lem13  8555  pwfseqlem1  8571  pwfseqlem5  8576  intgru  8727  addclpi  8807  addnidpi  8816  ltsonq  8884  nqpr  8929  reclem3pr  8964  recexsr  9020  supsrlem  9024  infmrcl  10025  nnnn0addcl  10289  un0addcl  10291  un0mulcl  10292  uzind3  10401  uzind3OLD  10403  uzind4  10572  zsupss  10603  rpnnen1lem1  10638  rpnnen1lem2  10639  rpnnen1lem3  10640  rpnnen1lem5  10642  ltsubrp  10681  ltaddrp  10682  xrlttr  10771  qbtwnxr  10824  xltnegi  10840  xaddnemnf  10858  xaddnepnf  10859  xaddcom  10862  xnegdi  10865  xsubge0  10878  xrub  10928  fzind2  11236  seqof  11418  expp1  11426  expneg  11427  expcllem  11430  mulexpz  11458  expaddz  11462  expmulz  11464  faclbnd4lem3  11624  faclbnd4  11626  brfi1uzind  11753  swrd00  11803  cats1un  11828  shftf  11932  sqrdiv  12109  leabs  12142  mulcn2  12427  summolem2  12548  fsumrev2  12603  geomulcvg  12691  ruclem6  12872  dvdseq  12935  dvdsfac  12942  gcdcllem1  13049  rpexp1i  13159  hashdvds  13202  iserodd  13247  pcqcl  13268  pcid  13284  ismred  13865  funcpropd  14135  natpropd  14211  latlem12  14545  clatl  14581  lubun  14588  odupos  14600  grpinvnzcl  14901  mulgneg  14946  mulgnn0z  14948  pgpssslw  15286  sylow2alem2  15290  sylow2a  15291  oddvdssubg  15508  gsumunsn  15582  gsum2d  15584  ablfac1eu  15669  pgpfac1lem5  15675  gsumdixp  15753  dvdsrcl2  15793  isdrngd  15898  evlslem4  16602  coe1tmmul2  16706  cnsubrg  16797  intcld  17142  neiptopnei  17234  ordtrest2lem  17305  lmss  17400  cmpcovf  17492  cncmp  17493  fincmp  17494  cmpsublem  17500  cmpsub  17501  uncon  17530  1stcfb  17546  2ndcsep  17560  1stckgenlem  17623  ptbasin  17647  ptbasfi  17651  ptunimpt  17665  ptuniconst  17668  dfac14  17688  ptcnp  17692  xkoptsub  17724  xkococnlem  17729  xkoinjcn  17757  qtopcmplem  17777  qtophmeo  17887  fbfinnfr  17911  isfcls  18079  psmettri2  18378  xmetrtri  18423  xmetrtri2  18424  blssioo  18864  divcn  18936  bndth  19021  resscdrg  19350  minveclem3  19368  finiunmbl  19476  opnmbllem  19531  ismbf2d  19569  itg2seq  19670  ellimc2  19802  limcmpt2  19809  limcres  19811  dvlem  19821  dvidlem  19840  dvrec  19879  dveflem  19901  dvlip  19915  coe1mul3  20060  dvtaylp  20324  leibpilem2  20819  leibpi  20820  wilthlem2  20890  basellem3  20903  dvdsflip  21005  dchreq  21080  dchrsum  21091  lgsval3  21136  lgsdir2lem4  21148  2sqlem6  21191  rpvmasumlem  21219  dchrisum0fno1  21243  rpvmasum2  21244  pntrsumbnd2  21299  ostthlem1  21359  umgraex  21396  usgraidx2vlem1  21448  nbgraf1olem3  21491  nbgraf1olem5  21493  cusconngra  21701  grpoidinvlem3  21832  ablo32  21912  ablomuldiv  21915  ablodivdiv  21916  ablodiv32  21918  nvadd12  22140  nvscom  22148  nvsubsub23  22181  dipassr  22385  htthlem  22458  hsn0elch  22788  shscli  22857  nmopun  23555  branmfn  23646  mdslj1i  23860  mdslj2i  23861  atss  23887  chcv1  23896  dmdbr5ati  23963  isoun  24124  esumsplit  24482  esumpcvgval  24503  sigaclcu2  24538  volmeas  24622  mbfmco2  24650  ballotlemfc0  24785  ballotlemfcc  24786  subfacp1lem4  24904  erdszelem7  24918  erdszelem8  24919  erdsze2lem2  24925  rescon  24968  cvmsdisj  24992  cvmscld  24995  climuzcnv  25143  prodmolem2  25296  zprod  25298  prodsn  25321  pocnv  25422  trpredmintr  25544  axcontlem2  25939  axcontlem7  25944  cgrid2  25972  btwncom  25983  btwnswapid2  25987  colinearperm1  26031  colinearperm3  26032  colinearperm2  26033  colinearperm4  26034  lineext  26045  colinbtwnle  26087  broutsideof2  26091  outsideofcom  26097  linecom  26119  linerflx2  26120  lineintmo  26126  bpolydiflem  26135  bpoly2  26138  bpoly3  26139  hfext  26159  opnmbllem0  26282  mblfinlem3  26285  mbfposadd  26294  itg2addnclem3  26300  bddiblnc  26317  ftc1anclem6  26327  ftc1anc  26330  ntruni  26372  clsint2  26374  locfincmp  26426  neibastop1  26430  eqfnun  26465  ac6gf  26476  heibor1lem  26560  isdrngo2  26616  unichnidl  26683  isfldidl  26720  ismrcd1  26864  isnacs3  26876  pellfundglb  27060  jm2.22  27178  jm2.23  27179  isnumbasgrplem1  27355  hbtlem6  27422  rngunsnply  27467  issubmd  27472  symgsssg  27497  symgfisg  27498  gsumcom3  27543  hashgcdlem  27605  phisum  27607  afv0nbfvbi  28103  nn0nndivcl  28262  nn0ge0div  28263  bnj521  29278  bnj926  29312  bnj1109  29331  bnj1294  29363  bnj545  29440  bnj605  29452  bnj594  29457  bnj934  29480  bnj953  29484  bnj1137  29538  bnj1174  29546  bnj1388  29576  lubunNEW  29945  lkrss2N  30141  elpadd0  30780  ltrnu  31092  tendoex  31946  cdlemm10N  32090  dicfnN  32155  dihmeetlem2N  32271  dihlatat  32309  lcfrlem9  32522
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 179  df-an 362
  Copyright terms: Public domain W3C validator