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  2420  eqtr3  2454  morex  3110  psssstr  3445  reuss2  3613  reupick  3617  reximdva0  3631  rabsneu  3871  opabss  4261  triun  4307  poirr  4506  wefrc  4568  ordsucuniel  4795  onzsl  4817  xpcan  5296  soex  5310  fnfco  5600  fun11iun  5686  suppssr  5855  eldmrexrnb  5868  fnressn  5909  fvtp3  5932  fvtp3g  5935  f1mpt  5998  offval  6303  dfoprab3  6394  1stconst  6426  2ndconst  6427  poxp  6449  fnwelem  6452  tfrlem2  6628  oeordsuc  6828  oelim2  6829  omsmolem  6887  fisucdomOLD  7303  ssnnfi  7319  fiint  7374  unifi  7386  indexfi  7405  iinfi  7413  unwdomg  7541  inf3lem5  7576  rankr1bg  7718  rankr1c  7736  carden2a  7842  dfac8clem  7902  dfac5lem4  7996  pwsdompw  8073  cfsuc  8126  cflim2  8132  enfin2i  8190  isf34lem4  8246  axdc4lem  8324  zornn0g  8374  uniimadomf  8409  fpwwe2lem8  8501  fpwwe2lem12  8505  fpwwe2lem13  8506  pwfseqlem1  8522  pwfseqlem5  8527  intgru  8678  addclpi  8758  addnidpi  8767  ltsonq  8835  nqpr  8880  reclem3pr  8915  recexsr  8971  supsrlem  8975  infmrcl  9976  nnnn0addcl  10240  un0addcl  10242  un0mulcl  10243  uzind3  10352  uzind3OLD  10354  uzind4  10523  zsupss  10554  rpnnen1lem1  10589  rpnnen1lem2  10590  rpnnen1lem3  10591  rpnnen1lem5  10593  ltsubrp  10632  ltaddrp  10633  xrlttr  10722  qbtwnxr  10775  xltnegi  10791  xaddnemnf  10809  xaddnepnf  10810  xaddcom  10813  xnegdi  10816  xsubge0  10829  xrub  10879  fzind2  11186  seqof  11368  expp1  11376  expneg  11377  expcllem  11380  mulexpz  11408  expaddz  11412  expmulz  11414  faclbnd4lem3  11574  faclbnd4  11576  brfi1uzind  11703  swrd00  11753  cats1un  11778  shftf  11882  sqrdiv  12059  leabs  12092  mulcn2  12377  summolem2  12498  fsumrev2  12553  geomulcvg  12641  ruclem6  12822  dvdseq  12885  dvdsfac  12892  gcdcllem1  12999  rpexp1i  13109  hashdvds  13152  iserodd  13197  pcqcl  13218  pcid  13234  ismred  13815  funcpropd  14085  natpropd  14161  latlem12  14495  clatl  14531  lubun  14538  odupos  14550  grpinvnzcl  14851  mulgneg  14896  mulgnn0z  14898  pgpssslw  15236  sylow2alem2  15240  sylow2a  15241  oddvdssubg  15458  gsumunsn  15532  gsum2d  15534  ablfac1eu  15619  pgpfac1lem5  15625  gsumdixp  15703  dvdsrcl2  15743  isdrngd  15848  evlslem4  16552  coe1tmmul2  16656  cnsubrg  16747  intcld  17092  neiptopnei  17184  ordtrest2lem  17255  lmss  17350  cmpcovf  17442  cncmp  17443  fincmp  17444  cmpsublem  17450  cmpsub  17451  uncon  17480  1stcfb  17496  2ndcsep  17510  1stckgenlem  17573  ptbasin  17597  ptbasfi  17601  ptunimpt  17615  ptuniconst  17618  dfac14  17638  ptcnp  17642  xkoptsub  17674  xkococnlem  17679  xkoinjcn  17707  qtopcmplem  17727  qtophmeo  17837  fbfinnfr  17861  isfcls  18029  psmettri2  18328  xmetrtri  18373  xmetrtri2  18374  blssioo  18814  divcn  18886  bndth  18971  resscdrg  19300  minveclem3  19318  finiunmbl  19426  opnmbllem  19481  ismbf2d  19521  itg2seq  19622  ellimc2  19752  limcmpt2  19759  limcres  19761  dvlem  19771  dvidlem  19790  dvrec  19829  dveflem  19851  dvlip  19865  coe1mul3  20010  dvtaylp  20274  leibpilem2  20769  leibpi  20770  wilthlem2  20840  basellem3  20853  dvdsflip  20955  dchreq  21030  dchrsum  21041  lgsval3  21086  lgsdir2lem4  21098  2sqlem6  21141  rpvmasumlem  21169  dchrisum0fno1  21193  rpvmasum2  21194  pntrsumbnd2  21249  ostthlem1  21309  umgraex  21346  usgraidx2vlem1  21398  nbgraf1olem3  21441  nbgraf1olem5  21443  cusconngra  21651  grpoidinvlem3  21782  ablo32  21862  ablomuldiv  21865  ablodivdiv  21866  ablodiv32  21868  nvadd12  22090  nvscom  22098  nvsubsub23  22131  dipassr  22335  htthlem  22408  hsn0elch  22738  shscli  22807  nmopun  23505  branmfn  23596  mdslj1i  23810  mdslj2i  23811  atss  23837  chcv1  23846  dmdbr5ati  23913  isoun  24077  esumsplit  24435  esumpcvgval  24456  sigaclcu2  24491  volmeas  24575  mbfmco2  24603  ballotlemfc0  24738  ballotlemfcc  24739  subfacp1lem4  24857  erdszelem7  24871  erdszelem8  24872  erdsze2lem2  24878  rescon  24921  cvmsdisj  24945  cvmscld  24948  climuzcnv  25096  prodmolem2  25250  zprod  25252  prodsn  25275  trpredmintr  25489  axcontlem2  25852  axcontlem7  25857  cgrid2  25885  btwncom  25896  btwnswapid2  25900  colinearperm1  25944  colinearperm3  25945  colinearperm2  25946  colinearperm4  25947  lineext  25958  colinbtwnle  26000  broutsideof2  26004  outsideofcom  26010  linecom  26032  linerflx2  26033  lineintmo  26039  bpolydiflem  26048  bpoly2  26051  bpoly3  26052  hfext  26072  mblfinlem2  26191  mbfposadd  26200  itg2addnclem3  26204  bddiblnc  26221  ntruni  26267  clsint2  26269  locfincmp  26321  neibastop1  26325  eqfnun  26360  ac6gf  26371  heibor1lem  26455  isdrngo2  26511  unichnidl  26578  isfldidl  26615  ismrcd1  26689  isnacs3  26701  pellfundglb  26885  jm2.22  27003  jm2.23  27004  isnumbasgrplem1  27181  hbtlem6  27248  rngunsnply  27293  issubmd  27298  symgsssg  27323  symgfisg  27324  gsumcom3  27369  hashgcdlem  27431  phisum  27433  afv0nbfvbi  27929  nn0nndivcl  28047  nn0ge0div  28048  bnj521  28958  bnj926  28992  bnj1109  29011  bnj1294  29043  bnj545  29120  bnj605  29132  bnj594  29137  bnj934  29160  bnj953  29164  bnj1137  29218  bnj1174  29226  bnj1388  29256  lubunNEW  29610  lkrss2N  29806  elpadd0  30445  ltrnu  30757  tendoex  31611  cdlemm10N  31755  dicfnN  31820  dihmeetlem2N  31936  dihlatat  31974  lcfrlem9  32187
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