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

Theorem sylan2b 461
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 186 . 2  |-  ( ph  ->  ch )
3 sylan2b.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan2 460 1  |-  ( ( ps  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  syl2anb  465  bm1.1  2268  eqtr3  2302  morex  2949  psssstr  3282  reuss2  3448  reupick  3452  reximdva0  3466  rabsneu  3702  opabss  4080  triun  4126  poirr  4325  wefrc  4387  ordsucuniel  4615  onzsl  4637  xpcan  5112  soex  5122  fnfco  5407  fun11iun  5493  suppssr  5659  fnressn  5705  fvtp3  5726  f1mpt  5785  offval  6085  dfoprab3  6176  1stconst  6207  2ndconst  6208  poxp  6227  fnwelem  6230  tfrlem2  6392  oeordsuc  6592  oelim2  6593  omsmolem  6651  fisucdomOLD  7066  ssnnfi  7082  fiint  7133  unifi  7145  indexfi  7163  iinfi  7171  unwdomg  7298  inf3lem5  7333  rankr1bg  7475  rankr1c  7493  carden2a  7599  dfac8clem  7659  dfac5lem4  7753  pwsdompw  7830  cfsuc  7883  cflim2  7889  enfin2i  7947  isf34lem4  8003  axdc4lem  8081  zornn0g  8132  uniimadomf  8167  fpwwe2lem8  8259  fpwwe2lem12  8263  fpwwe2lem13  8264  pwfseqlem1  8280  pwfseqlem5  8285  intgru  8436  addclpi  8516  addnidpi  8525  ltsonq  8593  nqpr  8638  reclem3pr  8673  recexsr  8729  supsrlem  8733  infmrcl  9733  nnnn0addcl  9995  un0addcl  9997  un0mulcl  9998  uzind3  10105  uzind3OLD  10107  uzind4  10276  zsupss  10307  rpnnen1lem1  10342  rpnnen1lem2  10343  rpnnen1lem3  10344  rpnnen1lem5  10346  ltsubrp  10385  ltaddrp  10386  xrlttr  10474  qbtwnxr  10527  xltnegi  10543  xaddnemnf  10561  xaddnepnf  10562  xaddcom  10565  xnegdi  10568  xsubge0  10581  xrub  10630  fzind2  10923  seqof  11103  expp1  11110  expneg  11111  expcllem  11114  mulexpz  11142  expaddz  11146  expmulz  11148  faclbnd4lem3  11308  faclbnd4  11310  swrd00  11451  cats1un  11476  shftf  11574  sqrdiv  11751  leabs  11784  mulcn2  12069  summolem2  12189  fsumrev2  12244  geomulcvg  12332  ruclem6  12513  dvdseq  12576  dvdsfac  12583  gcdcllem1  12690  rpexp1i  12800  hashdvds  12843  iserodd  12888  pcqcl  12909  pcid  12925  ismred  13504  funcpropd  13774  natpropd  13850  latlem12  14184  clatl  14220  lubun  14227  odupos  14239  grpinvnzcl  14540  mulgneg  14585  mulgnn0z  14587  pgpssslw  14925  sylow2alem2  14929  sylow2a  14930  oddvdssubg  15147  gsumunsn  15221  gsum2d  15223  ablfac1eu  15308  pgpfac1lem5  15314  gsumdixp  15392  dvdsrcl2  15432  isdrngd  15537  evlslem4  16245  coe1tmmul2  16352  cnsubrg  16432  intcld  16777  ordtrest2lem  16933  lmss  17026  cmpcovf  17118  cncmp  17119  fincmp  17120  cmpsublem  17126  cmpsub  17127  uncon  17155  1stcfb  17171  2ndcsep  17185  1stckgenlem  17248  ptbasin  17272  ptbasfi  17276  ptunimpt  17290  ptuniconst  17293  dfac14  17312  ptcnp  17316  xkoptsub  17348  xkococnlem  17353  xkoinjcn  17381  qtopcmplem  17398  qtophmeo  17508  fbfinnfr  17536  isfcls  17704  xmetrtri  17919  xmetrtri2  17920  blssioo  18301  divcn  18372  bndth  18456  resscdrg  18775  minveclem3  18793  finiunmbl  18901  opnmbllem  18956  ismbf2d  18996  itg2seq  19097  ellimc2  19227  limcmpt2  19234  limcres  19236  dvlem  19246  dvidlem  19265  dvrec  19304  dveflem  19326  dvlip  19340  coe1mul3  19485  dvtaylp  19749  leibpilem2  20237  leibpi  20238  wilthlem2  20307  basellem3  20320  dvdsflip  20422  dchreq  20497  dchrsum  20508  lgsval3  20553  lgsdir2lem4  20565  2sqlem6  20608  rpvmasumlem  20636  dchrisum0fno1  20660  rpvmasum2  20661  pntrsumbnd2  20716  ostthlem1  20776  grpoidinvlem3  20873  ablo32  20953  ablomuldiv  20956  ablodivdiv  20957  ablodiv32  20959  nvadd12  21179  nvscom  21187  nvsubsub23  21220  dipassr  21424  htthlem  21497  hsn0elch  21827  shscli  21896  nmopun  22594  branmfn  22685  mdslj1i  22899  mdslj2i  22900  atss  22926  chcv1  22935  dmdbr5ati  23002  ballotlemfc0  23051  ballotlemfcc  23052  isoun  23242  esumsplit  23431  esumpcvgval  23446  sigaclcu2  23481  mbfmco2  23570  subfacp1lem4  23714  erdszelem7  23728  erdszelem8  23729  erdsze2lem2  23735  rescon  23777  cvmsdisj  23801  cvmscld  23804  umgraex  23875  climuzcnv  24004  trpredmintr  24234  axcontlem2  24593  axcontlem7  24598  cgrid2  24626  btwncom  24637  btwnswapid2  24641  colinearperm1  24685  colinearperm3  24686  colinearperm2  24687  colinearperm4  24688  lineext  24699  colinbtwnle  24741  broutsideof2  24745  outsideofcom  24751  linecom  24773  linerflx2  24774  lineintmo  24780  bpolydiflem  24789  bpoly2  24792  bpoly3  24793  hfext  24813  copsexgb  24966  resid2  25097  preodom2  25226  preoran2  25230  toplat  25290  inttop3  25516  sallnei  25529  cmpidmor2  25969  gltpntl2  26073  ntruni  26245  clsint2  26247  locfincmp  26304  neibastop1  26308  eqfnun  26387  ac6gf  26411  heibor1lem  26533  isdrngo2  26589  unichnidl  26656  isfldidl  26693  ismrcd1  26773  isnacs3  26785  pellfundglb  26970  jm2.22  27088  jm2.23  27089  isnumbasgrplem1  27266  hbtlem6  27333  rngunsnply  27378  issubmd  27383  symgsssg  27408  symgfisg  27409  gsumcom3  27454  hashgcdlem  27516  phisum  27518  afv0nbfvbi  28014  bnj521  28765  bnj926  28799  bnj1109  28818  bnj1294  28850  bnj545  28927  bnj605  28939  bnj594  28944  bnj934  28967  bnj953  28971  bnj1137  29025  bnj1174  29033  bnj1388  29063  lubunNEW  29163  lkrss2N  29359  elpadd0  29998  ltrnu  30310  tendoex  31164  cdlemm10N  31308  dicfnN  31373  dihmeetlem2N  31489  dihlatat  31527  lcfrlem9  31740
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