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  2281  eqtr3  2315  morex  2962  psssstr  3295  reuss2  3461  reupick  3465  reximdva0  3479  rabsneu  3715  opabss  4096  triun  4142  poirr  4341  wefrc  4403  ordsucuniel  4631  onzsl  4653  xpcan  5128  soex  5138  fnfco  5423  fun11iun  5509  suppssr  5675  fnressn  5721  fvtp3  5742  f1mpt  5801  offval  6101  dfoprab3  6192  1stconst  6223  2ndconst  6224  poxp  6243  fnwelem  6246  tfrlem2  6408  oeordsuc  6608  oelim2  6609  omsmolem  6667  fisucdomOLD  7082  ssnnfi  7098  fiint  7149  unifi  7161  indexfi  7179  iinfi  7187  unwdomg  7314  inf3lem5  7349  rankr1bg  7491  rankr1c  7509  carden2a  7615  dfac8clem  7675  dfac5lem4  7769  pwsdompw  7846  cfsuc  7899  cflim2  7905  enfin2i  7963  isf34lem4  8019  axdc4lem  8097  zornn0g  8148  uniimadomf  8183  fpwwe2lem8  8275  fpwwe2lem12  8279  fpwwe2lem13  8280  pwfseqlem1  8296  pwfseqlem5  8301  intgru  8452  addclpi  8532  addnidpi  8541  ltsonq  8609  nqpr  8654  reclem3pr  8689  recexsr  8745  supsrlem  8749  infmrcl  9749  nnnn0addcl  10011  un0addcl  10013  un0mulcl  10014  uzind3  10121  uzind3OLD  10123  uzind4  10292  zsupss  10323  rpnnen1lem1  10358  rpnnen1lem2  10359  rpnnen1lem3  10360  rpnnen1lem5  10362  ltsubrp  10401  ltaddrp  10402  xrlttr  10490  qbtwnxr  10543  xltnegi  10559  xaddnemnf  10577  xaddnepnf  10578  xaddcom  10581  xnegdi  10584  xsubge0  10597  xrub  10646  fzind2  10939  seqof  11119  expp1  11126  expneg  11127  expcllem  11130  mulexpz  11158  expaddz  11162  expmulz  11164  faclbnd4lem3  11324  faclbnd4  11326  swrd00  11467  cats1un  11492  shftf  11590  sqrdiv  11767  leabs  11800  mulcn2  12085  summolem2  12205  fsumrev2  12260  geomulcvg  12348  ruclem6  12529  dvdseq  12592  dvdsfac  12599  gcdcllem1  12706  rpexp1i  12816  hashdvds  12859  iserodd  12904  pcqcl  12925  pcid  12941  ismred  13520  funcpropd  13790  natpropd  13866  latlem12  14200  clatl  14236  lubun  14243  odupos  14255  grpinvnzcl  14556  mulgneg  14601  mulgnn0z  14603  pgpssslw  14941  sylow2alem2  14945  sylow2a  14946  oddvdssubg  15163  gsumunsn  15237  gsum2d  15239  ablfac1eu  15324  pgpfac1lem5  15330  gsumdixp  15408  dvdsrcl2  15448  isdrngd  15553  evlslem4  16261  coe1tmmul2  16368  cnsubrg  16448  intcld  16793  ordtrest2lem  16949  lmss  17042  cmpcovf  17134  cncmp  17135  fincmp  17136  cmpsublem  17142  cmpsub  17143  uncon  17171  1stcfb  17187  2ndcsep  17201  1stckgenlem  17264  ptbasin  17288  ptbasfi  17292  ptunimpt  17306  ptuniconst  17309  dfac14  17328  ptcnp  17332  xkoptsub  17364  xkococnlem  17369  xkoinjcn  17397  qtopcmplem  17414  qtophmeo  17524  fbfinnfr  17552  isfcls  17720  xmetrtri  17935  xmetrtri2  17936  blssioo  18317  divcn  18388  bndth  18472  resscdrg  18791  minveclem3  18809  finiunmbl  18917  opnmbllem  18972  ismbf2d  19012  itg2seq  19113  ellimc2  19243  limcmpt2  19250  limcres  19252  dvlem  19262  dvidlem  19281  dvrec  19320  dveflem  19342  dvlip  19356  coe1mul3  19501  dvtaylp  19765  leibpilem2  20253  leibpi  20254  wilthlem2  20323  basellem3  20336  dvdsflip  20438  dchreq  20513  dchrsum  20524  lgsval3  20569  lgsdir2lem4  20581  2sqlem6  20624  rpvmasumlem  20652  dchrisum0fno1  20676  rpvmasum2  20677  pntrsumbnd2  20732  ostthlem1  20792  grpoidinvlem3  20889  ablo32  20969  ablomuldiv  20972  ablodivdiv  20973  ablodiv32  20975  nvadd12  21195  nvscom  21203  nvsubsub23  21236  dipassr  21440  htthlem  21513  hsn0elch  21843  shscli  21912  nmopun  22610  branmfn  22701  mdslj1i  22915  mdslj2i  22916  atss  22942  chcv1  22951  dmdbr5ati  23018  ballotlemfc0  23067  ballotlemfcc  23068  isoun  23257  esumsplit  23446  esumpcvgval  23461  sigaclcu2  23496  mbfmco2  23585  subfacp1lem4  23729  erdszelem7  23743  erdszelem8  23744  erdsze2lem2  23750  rescon  23792  cvmsdisj  23816  cvmscld  23819  umgraex  23890  climuzcnv  24019  prodmolem2  24158  zprod  24160  trpredmintr  24305  axcontlem2  24665  axcontlem7  24670  cgrid2  24698  btwncom  24709  btwnswapid2  24713  colinearperm1  24757  colinearperm3  24758  colinearperm2  24759  colinearperm4  24760  lineext  24771  colinbtwnle  24813  broutsideof2  24817  outsideofcom  24823  linecom  24845  linerflx2  24846  lineintmo  24852  bpolydiflem  24861  bpoly2  24864  bpoly3  24865  hfext  24885  bddiblnc  25021  copsexgb  25069  resid2  25200  preodom2  25329  preoran2  25333  toplat  25393  inttop3  25619  sallnei  25632  cmpidmor2  26072  gltpntl2  26176  ntruni  26348  clsint2  26350  locfincmp  26407  neibastop1  26411  eqfnun  26490  ac6gf  26514  heibor1lem  26636  isdrngo2  26692  unichnidl  26759  isfldidl  26796  ismrcd1  26876  isnacs3  26888  pellfundglb  27073  jm2.22  27191  jm2.23  27192  isnumbasgrplem1  27369  hbtlem6  27436  rngunsnply  27481  issubmd  27486  symgsssg  27511  symgfisg  27512  gsumcom3  27557  hashgcdlem  27619  phisum  27621  afv0nbfvbi  28119  bnj521  29081  bnj926  29115  bnj1109  29134  bnj1294  29166  bnj545  29243  bnj605  29255  bnj594  29260  bnj934  29283  bnj953  29287  bnj1137  29341  bnj1174  29349  bnj1388  29379  lubunNEW  29785  lkrss2N  29981  elpadd0  30620  ltrnu  30932  tendoex  31786  cdlemm10N  31930  dicfnN  31995  dihmeetlem2N  32111  dihlatat  32149  lcfrlem9  32362
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