MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimpi Structured version   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  1447  19.25  1613  sbbii  1665  spvw  1678  hbn1fw  1719  hbn1fwOLD  1720  excomim  1757  stdpc5  1816  equveli  2081  ax10-16  2266  exmoeu  2322  2mo  2358  eqeq1  2441  eleq2  2496  gencbvex  2990  moeq  3102  euind  3113  reuind  3129  eqsbc3r  3210  ssel  3334  unssd  3515  ssind  3557  n0moeu  3632  ss0  3650  uneqdifeq  3708  prprc  3908  ssunsn2  3950  eqsn  3952  trint  4309  snexALT  4377  snex  4397  pocl  4502  wefrc  4568  unexg  4702  unisn2  4703  reusv3i  4722  ordsson  4762  peano2  4857  brrelex12  4907  elrel  4970  dmxp  5080  xpssres  5172  elres  5173  elimasni  5223  dmsnsnsn  5340  coi2  5378  xpco  5406  iotabi  5419  uniabio  5420  iotaint  5423  nfunv  5476  funun  5487  funcnv3  5504  funimass1  5518  funssxp  5596  f1o00  5702  dffv3  5716  dffv2  5788  fndmin  5829  iinpreima  5852  fsn2  5900  ftpg  5908  fnsuppeq0  5945  isoselem  6053  oprabid  6097  1stval  6343  2ndval  6344  1stdm  6386  exopxfr2  6403  oprabco  6423  f1o2ndf1  6446  poxp  6450  sorpsscmpl  6525  riotaxfrd  6573  tz7.49c  6695  undifixp  7090  bren2  7130  ensym  7148  domunsn  7249  limenpsi  7274  php4  7286  isinf  7314  en2  7336  findcard2  7340  unfilem1  7363  fissuni  7403  elfiun  7427  marypha1lem  7430  marypha2lem3  7434  supmaxlem  7461  brwdom2  7533  brwdom3  7542  preleq  7564  inf3lem2  7576  tcmin  7672  rankvalb  7715  prwf  7729  r1pw  7763  rankuni2b  7771  rankr1id  7780  cardval3  7831  ficardom  7840  cardmin2  7877  isinfcard  7965  iscard3  7966  alephval3  7983  dfac9  8008  kmlem6  8027  ackbij1lem12  8103  fin23lem29  8213  fin23lem30  8214  fin23lem41  8224  isf32lem11  8235  isfin1-3  8258  fin1a2lem11  8282  fin1a2lem12  8283  fin1a2lem13  8284  axcc2lem  8308  dominf  8317  axdc4lem  8327  dominfac  8440  pwcfsdom  8450  cfpwsdom  8451  tskuni  8650  wfgru  8683  rpregt0  10617  xrrebnd  10748  xaddf  10802  supxrun  10886  elfz1end  11073  1fv  11112  elfznelfzob  11185  fzennn  11299  cardfz  11301  ser0  11367  crreczi  11496  faclbnd  11573  bcn1  11596  hashinfxadd  11651  hashge0  11653  hashssdif  11669  hashsnlei  11672  hashpw  11691  hashfun  11692  s4f1o  11857  sqr0  12039  cau3lem  12150  harmonic  12630  mertenslem2  12654  rpnnen2  12817  prmind2  13082  pceq0  13236  prmreclem6  13281  0ram  13380  ram0  13382  ressbas2  13512  ressinbas  13517  mrcuni  13838  mreexexlem4d  13864  catpropd  13927  arwhoma  14192  lubun  14542  psssdm  14640  plusfeq  14696  gsum2d  15538  staffn  15929  scafeq  15962  lbsexg  16228  lidldvgen  16318  ply1bascl2  16594  prmirred  16767  zlmassa  16797  frgpcyg  16846  ipfeq  16873  isbasis3g  17006  isopn2  17088  ntrval2  17107  toponmre  17149  innei  17181  restcld  17228  restcldi  17229  neitr  17236  discmp  17453  cmpsublem  17454  cmpsub  17455  2ndcctbss  17510  ptcnp  17646  imasnopn  17714  imasncld  17715  imasncls  17716  kqf  17771  fbun  17864  opnfbas  17866  cfinfil  17917  supfil  17919  ufprim  17933  acufl  17941  filufint  17944  ufldom  17986  hausflf2  18022  alexsubALTlem4  18073  cnextfval  18085  cnextfun  18087  cnextfres  18091  trust  18251  utoptop  18256  ustuqtop1  18263  metustidOLD  18581  metustid  18582  metustfbasOLD  18587  metustfbas  18588  cfilucfilOLD  18591  cfilucfil  18592  metustblOLD  18602  metustbl  18603  restmetu  18609  zlmclm  19112  cphassr  19166  ovolun  19387  volun  19431  dyadmax  19482  vitalilem2  19493  dvmptfsum  19851  rolle  19866  ulmcaulem  20302  logfac  20487  logno1  20519  logreclem  20652  leibpilem1  20772  prmorcht  20953  pclogsum  20991  2sqlem10  21150  chto1lb  21164  ausisusgra  21372  usgra2edg1  21395  usgrarnedg  21396  usgraedg4  21398  usgra1v  21401  usgraidx2vlem2  21403  usgraidx2v  21404  usgrares1  21416  nb3graprlem2  21453  nb3grapr  21454  nb3grapr2  21455  nb3gra2nb  21456  cusgra3v  21465  cusgrafilem2  21481  usgrasscusgra  21484  uvtxnbgra  21494  2trllemH  21544  2trllemE  21545  constr1trl  21580  fargshiftfo  21617  vdgrnn0pnf  21672  eupatrl  21682  grpoidinvlem3  21786  nmlno0lem  22286  blocni  22298  pythi  22343  normpythi  22636  isch3  22736  shmodsi  22883  omlsilem  22896  pjchi  22926  chlubii  22966  osumi  23136  nmlnop0iALT  23490  nmopun  23509  cnlnssadj  23575  nmopcoi  23590  mdbr3  23792  mdbr4  23793  ssmd1  23806  dmdsl3  23810  mdslmd1lem2  23821  mdslmd4i  23828  mdexchi  23830  atssma  23873  atoml2i  23878  chirredlem3  23887  mdsymlem1  23898  mdsymlem3  23900  dmdbr6ati  23918  dmdbr7ati  23919  cdjreui  23927  cdj3lem2b  23932  addltmulALT  23941  ssrmo  23973  iundifdif  24005  imadifxp  24030  fimacnvinrn2  24040  sspreima  24049  disjdsct  24082  xlt2addrd  24116  ressmulgnn0  24198  xrge0neqmnf  24204  xrge0nre  24205  kerunit  24253  pstmfval  24283  mndpluscn  24304  rge0scvg  24327  pnfneige0  24328  indval2  24404  esumnul  24435  gsumesum  24443  esumcst  24447  pwsiga  24505  insiga  24512  elsigagen2  24523  measxun2  24556  aean  24587  mbfmfun  24596  mbfmbfm  24600  1stmbfm  24602  2ndmbfm  24603  dya2iocnrect  24623  sibfof  24646  probun  24669  dstfrvclim1  24727  coinfliprv  24732  ballotlem2  24738  ballotlemfp1  24741  ballotlemic  24756  ballotlem1c  24757  cvmliftlem10  24973  ghomgrpilem2  25089  prodf1  25211  fprodfac  25288  risefacp1  25337  fallfacp1  25338  faclim  25357  dfon2lem3  25404  dfon2lem7  25408  dfon2lem8  25409  rdgprc0  25413  wfrlem4  25533  wfrlem5  25534  wfrlem10  25539  wfrlem15  25544  frrlem4  25577  frrlem5  25578  fvsingle  25757  unisnif  25762  funpartlem  25779  axcontlem7  25901  hfun  26111  df3nandALT1  26138  lukshef-ax2  26157  nandsym1  26164  mblfinlem  26234  mblfinlem2  26235  mblfinlem3  26236  ismblfin  26237  mbfresfi  26243  ftc1cnnc  26269  ftc1anclem6  26275  trer  26310  clsun  26322  opnregcld  26324  cldregopn  26325  ssref  26354  fnessref  26364  fnopabco  26415  frinfm  26428  nninfnub  26446  caushft  26458  bndss  26486  ispridl2  26639  istopclsd  26745  pellex  26889  rmspecsqrnq  26960  monotoddzzfi  26996  jm2.23  27058  expdioph  27085  dford3lem1  27088  wopprc  27092  inisegn0  27109  kelac1  27129  dfac21  27132  lsmfgcl  27140  pwssplit4  27159  dsmmbas2  27171  isnumbasgrp  27240  dgraalem  27318  en1uniel  27348  psgnunilem4  27388  pm10.12  27521  pm11.61  27560  sbiota1  27602  fnchoice  27667  fmuldfeq  27680  infrglb  27689  climsuselem1  27700  climsuse  27701  stoweidlem28  27744  stoweidlem48  27764  stoweidlem52  27768  stoweidlem57  27773  wallispilem3  27783  wallispilem4  27784  wallispi  27786  wallispi2lem1  27787  wallispi2lem2  27788  wallispi2  27789  stirlinglem7  27796  stirlinglem10  27799  stirlinglem12  27801  dandysum2p2e4  27910  2reu4a  27934  ndmaovrcl  28035  pr1eqbg  28046  f12dfv  28066  f13dfv  28067  euhash1  28145  addlenrevswrd  28157  swrd0swrd  28163  swrdswrd  28165  swrd0swrdid  28166  swrdccatin2  28176  swrdccatin12  28180  swrdccat3  28181  swrdccat3a  28183  cshwssizelem1a  28242  cshwsdisj  28248  cshwsiun  28249  usgra2wlkspthlem2  28260  usgra2pthlem1  28263  usgra2pth  28264  el2wlkonot  28289  el2spthonot  28290  el2wlkonotot0  28292  frgra3v  28329  3vfriswmgra  28332  1to3vfriswmgra  28334  1to3vfriendship  28335  2pthfrgra  28338  4cycl2v2nb  28343  n4cyclfrgra  28345  frgranbnb  28347  frgrancvvdeqlem4  28359  frgrawopreg  28375  frg2woteqm  28385  usg2spot2nb  28391  biimp  28501  bi2imp  28502  bi3impb  28503  bi3impa  28504  bi13impib  28506  bi123impib  28507  bi13impia  28508  bi123impia  28509  bi13imp23  28512  bi13imp2  28513  bi12imp3  28514  dfvd1imp  28604  dfvd2imp  28641  e1bi  28667  e2bi  28670  e3bi  28787  3ornot23VD  28896  3impexpbicomVD  28906  3impexpbicomiVD  28907  tratrbVD  28910  ssralv2VD  28915  equncomiVD  28918  truniALTVD  28927  ee33VD  28928  csbingVD  28933  onfrALTlem3VD  28936  onfrALTlem2VD  28938  onfrALTlem1VD  28939  onfrALTVD  28940  csbsngVD  28942  csbxpgVD  28943  csbrngVD  28945  csbunigVD  28947  csbfv12gALTVD  28948  relopabVD  28950  2uasbanhVD  28960  vk15.4jVD  28963  unisnALT  28975  chordthmALT  28982  iunconlem2  28984  bnj529  29046  bnj927  29076  bnj1379  29139  bnj1424  29147  bnj1436  29148  bnj1476  29155  bnj607  29224  bnj849  29233  bnj908  29239  bnj1097  29287  bnj1118  29290  bnj1128  29296  bnj1145  29299  bnj1154  29305  bnj1174  29309  bnj1189  29315  bnj1204  29318  bnj1279  29324  bnj1388  29339  bnj1417  29347  ax7w10AUX7  29599  lubunNEW  29708  lkr0f  29829  glbconN  30111  paddssat  30548  pclunN  30632  2polssN  30649  paddunN  30661  poldmj1N  30662  ltrnnid  30870  dibglbN  31901
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