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  1660  spvw  1673  hbn1fw  1712  excomim  1749  stdpc5  1806  ax10-16  2217  exmoeu  2273  2mo  2309  eqeq1  2386  eleq2  2441  gencbvex  2934  moeq  3046  euind  3057  reuind  3073  eqsbc3r  3154  ssel  3278  unssd  3459  ssind  3501  n0moeu  3576  ss0  3594  uneqdifeq  3652  prprc  3852  ssunsn2  3894  eqsn  3896  trint  4251  snexALT  4319  snex  4339  pocl  4444  wefrc  4510  unexg  4643  unisn2  4644  reusv3i  4663  ordsson  4703  peano2  4798  brrelex12  4848  elrel  4911  dmxp  5021  xpssres  5113  elres  5114  elimasni  5164  dmsnsnsn  5281  coi2  5319  xpco  5347  iotabi  5360  uniabio  5361  iotaint  5364  nfunv  5417  funun  5428  funcnv3  5445  funimass1  5459  funssxp  5537  f1o00  5643  dffv3  5657  dffv2  5728  fndmin  5769  iinpreima  5792  fsn2  5840  ftpg  5848  fnsuppeq0  5885  isoselem  5993  oprabid  6037  1stval  6283  2ndval  6284  1stdm  6326  exopxfr2  6343  oprabco  6363  poxp  6387  sorpsscmpl  6462  riotaxfrd  6510  tz7.49c  6632  undifixp  7027  bren2  7067  ensym  7085  domunsn  7186  limenpsi  7211  php4  7223  isinf  7251  en2  7273  findcard2  7277  unfilem1  7300  fissuni  7339  elfiun  7363  marypha1lem  7366  marypha2lem3  7370  supmaxlem  7395  brwdom2  7467  brwdom3  7476  preleq  7498  inf3lem2  7510  tcmin  7606  rankvalb  7649  prwf  7663  r1pw  7697  rankuni2b  7705  rankr1id  7714  cardval3  7765  ficardom  7774  cardmin2  7811  isinfcard  7899  iscard3  7900  alephval3  7917  dfac9  7942  kmlem6  7961  ackbij1lem12  8037  fin23lem29  8147  fin23lem30  8148  fin23lem41  8158  isf32lem11  8169  isfin1-3  8192  fin1a2lem11  8216  fin1a2lem12  8217  fin1a2lem13  8218  axcc2lem  8242  dominf  8251  axdc4lem  8261  dominfac  8374  pwcfsdom  8384  cfpwsdom  8385  tskuni  8584  wfgru  8617  rpregt0  10550  xrrebnd  10681  xaddf  10735  supxrun  10819  elfz1end  11006  1fv  11043  elfznelfzob  11113  fzennn  11227  cardfz  11229  ser0  11295  crreczi  11424  faclbnd  11501  bcn1  11524  hashinfxadd  11579  hashge0  11581  hashssdif  11597  hashsnlei  11600  hashpw  11619  hashfun  11620  s4f1o  11785  sqr0  11967  cau3lem  12078  harmonic  12558  mertenslem2  12582  rpnnen2  12745  prmind2  13010  pceq0  13164  prmreclem6  13209  0ram  13308  ram0  13310  ressbas2  13440  ressinbas  13445  mrcuni  13766  mreexexlem4d  13792  catpropd  13855  arwhoma  14120  lubun  14470  psssdm  14568  plusfeq  14624  gsum2d  15466  staffn  15857  scafeq  15890  lbsexg  16156  lidldvgen  16246  ply1bascl2  16522  prmirred  16691  zlmassa  16721  frgpcyg  16770  ipfeq  16797  isbasis3g  16930  isopn2  17012  ntrval2  17031  toponmre  17073  innei  17105  restcld  17151  restcldi  17152  neitr  17159  discmp  17376  cmpsublem  17377  cmpsub  17378  2ndcctbss  17432  ptcnp  17568  imasnopn  17636  imasncld  17637  imasncls  17638  kqf  17693  fbun  17786  opnfbas  17788  cfinfil  17839  supfil  17841  ufprim  17855  acufl  17863  filufint  17866  ufldom  17908  hausflf2  17944  alexsubALTlem4  17995  cnextfval  18007  cnextfun  18009  cnextfres  18013  trust  18173  utoptop  18178  ustuqtop1  18185  metustid  18467  metustfbas  18470  cfilucfil  18472  metustbl  18479  restmetu  18482  zlmclm  18984  cphassr  19038  ovolun  19255  volun  19299  dyadmax  19350  vitalilem2  19361  dvmptfsum  19719  rolle  19734  ulmcaulem  20170  logfac  20355  logno1  20387  logreclem  20520  leibpilem1  20640  prmorcht  20821  pclogsum  20859  2sqlem10  21018  chto1lb  21032  ausisusgra  21240  usgra2edg1  21262  usgrarnedg  21263  usgraedg4  21265  usgra1v  21268  usgraidx2vlem2  21270  usgraidx2v  21271  usgrares1  21283  nb3graprlem2  21320  nb3grapr  21321  nb3grapr2  21322  nb3gra2nb  21323  cusgra3v  21332  cusgrafilem2  21348  usgrasscusgra  21351  uvtxnbgra  21361  constr1trl  21429  constr2trl  21439  fargshiftfo  21466  vdgrnn0pnf  21521  eupatrl  21531  grpoidinvlem3  21635  nmlno0lem  22135  blocni  22147  pythi  22192  normpythi  22485  isch3  22585  shmodsi  22732  omlsilem  22745  pjchi  22775  chlubii  22815  osumi  22985  nmlnop0iALT  23339  nmopun  23358  cnlnssadj  23424  nmopcoi  23439  mdbr3  23641  mdbr4  23642  ssmd1  23655  dmdsl3  23659  mdslmd1lem2  23670  mdslmd4i  23677  mdexchi  23679  atssma  23722  atoml2i  23727  chirredlem3  23736  mdsymlem1  23747  mdsymlem3  23749  dmdbr6ati  23767  dmdbr7ati  23768  cdjreui  23776  cdj3lem2b  23781  addltmulALT  23790  ssrmo  23818  iundifdif  23850  imadifxp  23874  fimacnvinrn2  23884  sspreima  23892  disjdsct  23924  xlt2addrd  23953  ressmulgnn0  24028  xrge0neqmnf  24034  xrge0nre  24035  kerunit  24070  mndpluscn  24109  rge0scvg  24132  pnfneige0  24133  indval2  24201  esumnul  24232  gsumesum  24240  esumcst  24244  pwsiga  24302  insiga  24309  elsigagen2  24320  measxun2  24351  aean  24382  mbfmfun  24391  mbfmbfm  24395  1stmbfm  24397  2ndmbfm  24398  dya2iocnrect  24418  probun  24449  dstfrvclim1  24507  coinfliprv  24512  ballotlem2  24518  ballotlemfp1  24521  ballotlemic  24536  ballotlem1c  24537  cvmliftlem10  24753  ghomgrpilem2  24869  prodf1  24991  fprodfac  25068  risefacp1  25106  fallfacp1  25107  faclim  25116  dfon2lem3  25158  dfon2lem7  25162  dfon2lem8  25163  rdgprc0  25167  wfrlem4  25276  wfrlem5  25277  wfrlem10  25282  wfrlem15  25287  frrlem4  25301  frrlem5  25302  unisnif  25481  funpartlem  25498  axcontlem7  25616  hfun  25826  df3nandALT1  25853  lukshef-ax2  25872  nandsym1  25879  ftc1cnnc  25972  trer  26003  clsun  26015  opnregcld  26017  cldregopn  26018  ssref  26047  fnessref  26057  fnopabco  26108  frinfm  26121  nninfnub  26139  caushft  26151  bndss  26179  ispridl2  26332  istopclsd  26438  pellex  26582  rmspecsqrnq  26653  monotoddzzfi  26689  jm2.23  26751  expdioph  26778  dford3lem1  26781  wopprc  26785  inisegn0  26802  kelac1  26823  dfac21  26826  lsmfgcl  26834  pwssplit4  26853  dsmmbas2  26865  isnumbasgrp  26934  dgraalem  27012  en1uniel  27042  psgnunilem4  27082  pm10.12  27215  pm11.61  27254  sbiota1  27296  fnchoice  27361  fmuldfeq  27374  infrglb  27383  climsuselem1  27394  climsuse  27395  stoweidlem28  27438  stoweidlem48  27458  stoweidlem52  27462  stoweidlem57  27467  wallispilem3  27477  wallispilem4  27478  wallispi  27480  wallispi2lem1  27481  wallispi2lem2  27482  wallispi2  27483  stirlinglem7  27490  stirlinglem10  27493  stirlinglem12  27495  dandysum2p2e4  27604  2reu4a  27628  ndmaovrcl  27730  frgra3v  27748  3vfriswmgra  27751  1to3vfriswmgra  27753  1to3vfriendship  27754  2pthfrgra  27757  4cycl2v2nb  27762  n4cyclfrgra  27764  frgranbnb  27766  frgrancvvdeqlem4  27778  frgrawopreg  27794  biimp  27903  bi2imp  27904  bi3impb  27905  bi3impa  27906  bi13impib  27908  bi123impib  27909  bi13impia  27910  bi123impia  27911  bi13imp23  27914  bi13imp2  27915  bi12imp3  27916  dfvd1imp  28001  dfvd2imp  28038  e1bi  28064  e2bi  28067  e3bi  28184  3ornot23VD  28293  3impexpbicomVD  28303  3impexpbicomiVD  28304  tratrbVD  28307  ssralv2VD  28312  equncomiVD  28315  truniALTVD  28324  ee33VD  28325  csbingVD  28330  onfrALTlem3VD  28333  onfrALTlem2VD  28335  onfrALTlem1VD  28336  onfrALTVD  28337  csbsngVD  28339  csbxpgVD  28340  csbrngVD  28342  csbunigVD  28344  csbfv12gALTVD  28345  relopabVD  28347  2uasbanhVD  28357  vk15.4jVD  28360  unisnALT  28372  chordthmALT  28380  bnj529  28440  bnj927  28470  bnj1379  28533  bnj1424  28541  bnj1436  28542  bnj1476  28549  bnj607  28618  bnj849  28627  bnj908  28633  bnj1097  28681  bnj1118  28684  bnj1128  28690  bnj1145  28693  bnj1154  28699  bnj1174  28703  bnj1189  28709  bnj1204  28712  bnj1279  28718  bnj1388  28733  bnj1417  28741  ax12OLD  29081  lubunNEW  29139  lkr0f  29260  glbconN  29542  paddssat  29979  pclunN  30063  2polssN  30080  paddunN  30092  poldmj1N  30093  ltrnnid  30301  dibglbN  31332
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