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

Theorem biimpi 187
Description: Infer an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
biimpi.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
biimpi  |-  ( ph  ->  ps )

Proof of Theorem biimpi
StepHypRef Expression
1 biimpi.1 . 2  |-  ( ph  <->  ps )
2 bi1 179 . 2  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
31, 2ax-mp 8 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  sylbi  188  sylib  189  biimpri  198  mpbi  200  syl5bi  209  syl6ib  218  syl7bi  222  syl8ib  223  bitri  241  pm2.53  363  simplbi  447  simprbi  451  sylanb  459  sylan2b  462  pm3.1  485  orbi2i  506  pm2.32  513  anc2l  539  pm3.37  563  dfbi  611  pm2.76  822  pm5.15  860  pm5.16  861  pm5.75  904  rnlem  932  simp1bi  972  simp2bi  973  simp3bi  974  syl3an1b  1220  syl3an2b  1221  syl3an3b  1222  nic-ax  1444  19.25  1610  sbbii  1661  spvw  1674  hbn1fw  1715  hbn1fwOLD  1716  excomim  1753  stdpc5  1812  equveli  2042  ax10-16  2240  exmoeu  2296  2mo  2332  eqeq1  2410  eleq2  2465  gencbvex  2958  moeq  3070  euind  3081  reuind  3097  eqsbc3r  3178  ssel  3302  unssd  3483  ssind  3525  n0moeu  3600  ss0  3618  uneqdifeq  3676  prprc  3876  ssunsn2  3918  eqsn  3920  trint  4277  snexALT  4345  snex  4365  pocl  4470  wefrc  4536  unexg  4669  unisn2  4670  reusv3i  4689  ordsson  4729  peano2  4824  brrelex12  4874  elrel  4937  dmxp  5047  xpssres  5139  elres  5140  elimasni  5190  dmsnsnsn  5307  coi2  5345  xpco  5373  iotabi  5386  uniabio  5387  iotaint  5390  nfunv  5443  funun  5454  funcnv3  5471  funimass1  5485  funssxp  5563  f1o00  5669  dffv3  5683  dffv2  5755  fndmin  5796  iinpreima  5819  fsn2  5867  ftpg  5875  fnsuppeq0  5912  isoselem  6020  oprabid  6064  1stval  6310  2ndval  6311  1stdm  6353  exopxfr2  6370  oprabco  6390  f1o2ndf1  6413  poxp  6417  sorpsscmpl  6492  riotaxfrd  6540  tz7.49c  6662  undifixp  7057  bren2  7097  ensym  7115  domunsn  7216  limenpsi  7241  php4  7253  isinf  7281  en2  7303  findcard2  7307  unfilem1  7330  fissuni  7369  elfiun  7393  marypha1lem  7396  marypha2lem3  7400  supmaxlem  7425  brwdom2  7497  brwdom3  7506  preleq  7528  inf3lem2  7540  tcmin  7636  rankvalb  7679  prwf  7693  r1pw  7727  rankuni2b  7735  rankr1id  7744  cardval3  7795  ficardom  7804  cardmin2  7841  isinfcard  7929  iscard3  7930  alephval3  7947  dfac9  7972  kmlem6  7991  ackbij1lem12  8067  fin23lem29  8177  fin23lem30  8178  fin23lem41  8188  isf32lem11  8199  isfin1-3  8222  fin1a2lem11  8246  fin1a2lem12  8247  fin1a2lem13  8248  axcc2lem  8272  dominf  8281  axdc4lem  8291  dominfac  8404  pwcfsdom  8414  cfpwsdom  8415  tskuni  8614  wfgru  8647  rpregt0  10581  xrrebnd  10712  xaddf  10766  supxrun  10850  elfz1end  11037  1fv  11075  elfznelfzob  11148  fzennn  11262  cardfz  11264  ser0  11330  crreczi  11459  faclbnd  11536  bcn1  11559  hashinfxadd  11614  hashge0  11616  hashssdif  11632  hashsnlei  11635  hashpw  11654  hashfun  11655  s4f1o  11820  sqr0  12002  cau3lem  12113  harmonic  12593  mertenslem2  12617  rpnnen2  12780  prmind2  13045  pceq0  13199  prmreclem6  13244  0ram  13343  ram0  13345  ressbas2  13475  ressinbas  13480  mrcuni  13801  mreexexlem4d  13827  catpropd  13890  arwhoma  14155  lubun  14505  psssdm  14603  plusfeq  14659  gsum2d  15501  staffn  15892  scafeq  15925  lbsexg  16191  lidldvgen  16281  ply1bascl2  16557  prmirred  16730  zlmassa  16760  frgpcyg  16809  ipfeq  16836  isbasis3g  16969  isopn2  17051  ntrval2  17070  toponmre  17112  innei  17144  restcld  17190  restcldi  17191  neitr  17198  discmp  17415  cmpsublem  17416  cmpsub  17417  2ndcctbss  17471  ptcnp  17607  imasnopn  17675  imasncld  17676  imasncls  17677  kqf  17732  fbun  17825  opnfbas  17827  cfinfil  17878  supfil  17880  ufprim  17894  acufl  17902  filufint  17905  ufldom  17947  hausflf2  17983  alexsubALTlem4  18034  cnextfval  18046  cnextfun  18048  cnextfres  18052  trust  18212  utoptop  18217  ustuqtop1  18224  metustidOLD  18542  metustid  18543  metustfbasOLD  18548  metustfbas  18549  cfilucfilOLD  18552  cfilucfil  18553  metustblOLD  18563  metustbl  18564  restmetu  18570  zlmclm  19073  cphassr  19127  ovolun  19348  volun  19392  dyadmax  19443  vitalilem2  19454  dvmptfsum  19812  rolle  19827  ulmcaulem  20263  logfac  20448  logno1  20480  logreclem  20613  leibpilem1  20733  prmorcht  20914  pclogsum  20952  2sqlem10  21111  chto1lb  21125  ausisusgra  21333  usgra2edg1  21356  usgrarnedg  21357  usgraedg4  21359  usgra1v  21362  usgraidx2vlem2  21364  usgraidx2v  21365  usgrares1  21377  nb3graprlem2  21414  nb3grapr  21415  nb3grapr2  21416  nb3gra2nb  21417  cusgra3v  21426  cusgrafilem2  21442  usgrasscusgra  21445  uvtxnbgra  21455  2trllemH  21505  2trllemE  21506  constr1trl  21541  fargshiftfo  21578  vdgrnn0pnf  21633  eupatrl  21643  grpoidinvlem3  21747  nmlno0lem  22247  blocni  22259  pythi  22304  normpythi  22597  isch3  22697  shmodsi  22844  omlsilem  22857  pjchi  22887  chlubii  22927  osumi  23097  nmlnop0iALT  23451  nmopun  23470  cnlnssadj  23536  nmopcoi  23551  mdbr3  23753  mdbr4  23754  ssmd1  23767  dmdsl3  23771  mdslmd1lem2  23782  mdslmd4i  23789  mdexchi  23791  atssma  23834  atoml2i  23839  chirredlem3  23848  mdsymlem1  23859  mdsymlem3  23861  dmdbr6ati  23879  dmdbr7ati  23880  cdjreui  23888  cdj3lem2b  23893  addltmulALT  23902  ssrmo  23934  iundifdif  23966  imadifxp  23991  fimacnvinrn2  24001  sspreima  24010  disjdsct  24043  xlt2addrd  24077  ressmulgnn0  24159  xrge0neqmnf  24165  xrge0nre  24166  kerunit  24214  pstmfval  24244  mndpluscn  24265  rge0scvg  24288  pnfneige0  24289  indval2  24365  esumnul  24396  gsumesum  24404  esumcst  24408  pwsiga  24466  insiga  24473  elsigagen2  24484  measxun2  24517  aean  24548  mbfmfun  24557  mbfmbfm  24561  1stmbfm  24563  2ndmbfm  24564  dya2iocnrect  24584  sibfof  24607  probun  24630  dstfrvclim1  24688  coinfliprv  24693  ballotlem2  24699  ballotlemfp1  24702  ballotlemic  24717  ballotlem1c  24718  cvmliftlem10  24934  ghomgrpilem2  25050  prodf1  25172  fprodfac  25249  risefacp1  25297  fallfacp1  25298  faclim  25313  dfon2lem3  25355  dfon2lem7  25359  dfon2lem8  25360  rdgprc0  25364  wfrlem4  25473  wfrlem5  25474  wfrlem10  25479  wfrlem15  25484  frrlem4  25498  frrlem5  25499  unisnif  25678  funpartlem  25695  axcontlem7  25813  hfun  26023  df3nandALT1  26050  lukshef-ax2  26069  nandsym1  26076  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  mbfresfi  26152  ftc1cnnc  26178  trer  26209  clsun  26221  opnregcld  26223  cldregopn  26224  ssref  26253  fnessref  26263  fnopabco  26314  frinfm  26327  nninfnub  26345  caushft  26357  bndss  26385  ispridl2  26538  istopclsd  26644  pellex  26788  rmspecsqrnq  26859  monotoddzzfi  26895  jm2.23  26957  expdioph  26984  dford3lem1  26987  wopprc  26991  inisegn0  27008  kelac1  27029  dfac21  27032  lsmfgcl  27040  pwssplit4  27059  dsmmbas2  27071  isnumbasgrp  27140  dgraalem  27218  en1uniel  27248  psgnunilem4  27288  pm10.12  27421  pm11.61  27460  sbiota1  27502  fnchoice  27567  fmuldfeq  27580  infrglb  27589  climsuselem1  27600  climsuse  27601  stoweidlem28  27644  stoweidlem48  27664  stoweidlem52  27668  stoweidlem57  27673  wallispilem3  27683  wallispilem4  27684  wallispi  27686  wallispi2lem1  27687  wallispi2lem2  27688  wallispi2  27689  stirlinglem7  27696  stirlinglem10  27699  stirlinglem12  27701  dandysum2p2e4  27810  2reu4a  27834  ndmaovrcl  27935  pr1eqbg  27944  f12dfv  27961  f13dfv  27962  euhash1  27998  addlenrevswrd  28004  swrd0swrd  28009  swrdswrd  28011  swrd0swrdid  28012  swrdccatin2  28018  swrdccat3a  28030  swrdccat3b  28031  usgra2wlkspthlem2  28037  usgra2pthlem1  28040  usgra2pth  28041  el2wlkonot  28066  el2spthonot  28067  el2wlkonotot0  28069  frgra3v  28106  3vfriswmgra  28109  1to3vfriswmgra  28111  1to3vfriendship  28112  2pthfrgra  28115  4cycl2v2nb  28120  n4cyclfrgra  28122  frgranbnb  28124  frgrancvvdeqlem4  28136  frgrawopreg  28152  frg2woteqm  28162  usg2spot2nb  28168  biimp  28278  bi2imp  28279  bi3impb  28280  bi3impa  28281  bi13impib  28283  bi123impib  28284  bi13impia  28285  bi123impia  28286  bi13imp23  28289  bi13imp2  28290  bi12imp3  28291  dfvd1imp  28376  dfvd2imp  28413  e1bi  28439  e2bi  28442  e3bi  28559  3ornot23VD  28668  3impexpbicomVD  28678  3impexpbicomiVD  28679  tratrbVD  28682  ssralv2VD  28687  equncomiVD  28690  truniALTVD  28699  ee33VD  28700  csbingVD  28705  onfrALTlem3VD  28708  onfrALTlem2VD  28710  onfrALTlem1VD  28711  onfrALTVD  28712  csbsngVD  28714  csbxpgVD  28715  csbrngVD  28717  csbunigVD  28719  csbfv12gALTVD  28720  relopabVD  28722  2uasbanhVD  28732  vk15.4jVD  28735  unisnALT  28747  chordthmALT  28755  bnj529  28815  bnj927  28845  bnj1379  28908  bnj1424  28916  bnj1436  28917  bnj1476  28924  bnj607  28993  bnj849  29002  bnj908  29008  bnj1097  29056  bnj1118  29059  bnj1128  29065  bnj1145  29068  bnj1154  29074  bnj1174  29078  bnj1189  29084  bnj1204  29087  bnj1279  29093  bnj1388  29108  bnj1417  29116  lubunNEW  29456  lkr0f  29577  glbconN  29859  paddssat  30296  pclunN  30380  2polssN  30397  paddunN  30409  poldmj1N  30410  ltrnnid  30618  dibglbN  31649
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
  Copyright terms: Public domain W3C validator