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  2225  exmoeu  2281  2mo  2317  eqeq1  2394  eleq2  2449  gencbvex  2942  moeq  3054  euind  3065  reuind  3081  eqsbc3r  3162  ssel  3286  unssd  3467  ssind  3509  n0moeu  3584  ss0  3602  uneqdifeq  3660  prprc  3860  ssunsn2  3902  eqsn  3904  trint  4259  snexALT  4327  snex  4347  pocl  4452  wefrc  4518  unexg  4651  unisn2  4652  reusv3i  4671  ordsson  4711  peano2  4806  brrelex12  4856  elrel  4919  dmxp  5029  xpssres  5121  elres  5122  elimasni  5172  dmsnsnsn  5289  coi2  5327  xpco  5355  iotabi  5368  uniabio  5369  iotaint  5372  nfunv  5425  funun  5436  funcnv3  5453  funimass1  5467  funssxp  5545  f1o00  5651  dffv3  5665  dffv2  5736  fndmin  5777  iinpreima  5800  fsn2  5848  ftpg  5856  fnsuppeq0  5893  isoselem  6001  oprabid  6045  1stval  6291  2ndval  6292  1stdm  6334  exopxfr2  6351  oprabco  6371  poxp  6395  sorpsscmpl  6470  riotaxfrd  6518  tz7.49c  6640  undifixp  7035  bren2  7075  ensym  7093  domunsn  7194  limenpsi  7219  php4  7231  isinf  7259  en2  7281  findcard2  7285  unfilem1  7308  fissuni  7347  elfiun  7371  marypha1lem  7374  marypha2lem3  7378  supmaxlem  7403  brwdom2  7475  brwdom3  7484  preleq  7506  inf3lem2  7518  tcmin  7614  rankvalb  7657  prwf  7671  r1pw  7705  rankuni2b  7713  rankr1id  7722  cardval3  7773  ficardom  7782  cardmin2  7819  isinfcard  7907  iscard3  7908  alephval3  7925  dfac9  7950  kmlem6  7969  ackbij1lem12  8045  fin23lem29  8155  fin23lem30  8156  fin23lem41  8166  isf32lem11  8177  isfin1-3  8200  fin1a2lem11  8224  fin1a2lem12  8225  fin1a2lem13  8226  axcc2lem  8250  dominf  8259  axdc4lem  8269  dominfac  8382  pwcfsdom  8392  cfpwsdom  8393  tskuni  8592  wfgru  8625  rpregt0  10558  xrrebnd  10689  xaddf  10743  supxrun  10827  elfz1end  11014  1fv  11051  elfznelfzob  11121  fzennn  11235  cardfz  11237  ser0  11303  crreczi  11432  faclbnd  11509  bcn1  11532  hashinfxadd  11587  hashge0  11589  hashssdif  11605  hashsnlei  11608  hashpw  11627  hashfun  11628  s4f1o  11793  sqr0  11975  cau3lem  12086  harmonic  12566  mertenslem2  12590  rpnnen2  12753  prmind2  13018  pceq0  13172  prmreclem6  13217  0ram  13316  ram0  13318  ressbas2  13448  ressinbas  13453  mrcuni  13774  mreexexlem4d  13800  catpropd  13863  arwhoma  14128  lubun  14478  psssdm  14576  plusfeq  14632  gsum2d  15474  staffn  15865  scafeq  15898  lbsexg  16164  lidldvgen  16254  ply1bascl2  16530  prmirred  16699  zlmassa  16729  frgpcyg  16778  ipfeq  16805  isbasis3g  16938  isopn2  17020  ntrval2  17039  toponmre  17081  innei  17113  restcld  17159  restcldi  17160  neitr  17167  discmp  17384  cmpsublem  17385  cmpsub  17386  2ndcctbss  17440  ptcnp  17576  imasnopn  17644  imasncld  17645  imasncls  17646  kqf  17701  fbun  17794  opnfbas  17796  cfinfil  17847  supfil  17849  ufprim  17863  acufl  17871  filufint  17874  ufldom  17916  hausflf2  17952  alexsubALTlem4  18003  cnextfval  18015  cnextfun  18017  cnextfres  18021  trust  18181  utoptop  18186  ustuqtop1  18193  metustid  18475  metustfbas  18478  cfilucfil  18480  metustbl  18487  restmetu  18490  zlmclm  18992  cphassr  19046  ovolun  19263  volun  19307  dyadmax  19358  vitalilem2  19369  dvmptfsum  19727  rolle  19742  ulmcaulem  20178  logfac  20363  logno1  20395  logreclem  20528  leibpilem1  20648  prmorcht  20829  pclogsum  20867  2sqlem10  21026  chto1lb  21040  ausisusgra  21248  usgra2edg1  21270  usgrarnedg  21271  usgraedg4  21273  usgra1v  21276  usgraidx2vlem2  21278  usgraidx2v  21279  usgrares1  21291  nb3graprlem2  21328  nb3grapr  21329  nb3grapr2  21330  nb3gra2nb  21331  cusgra3v  21340  cusgrafilem2  21356  usgrasscusgra  21359  uvtxnbgra  21369  constr1trl  21437  constr2trl  21447  fargshiftfo  21474  vdgrnn0pnf  21529  eupatrl  21539  grpoidinvlem3  21643  nmlno0lem  22143  blocni  22155  pythi  22200  normpythi  22493  isch3  22593  shmodsi  22740  omlsilem  22753  pjchi  22783  chlubii  22823  osumi  22993  nmlnop0iALT  23347  nmopun  23366  cnlnssadj  23432  nmopcoi  23447  mdbr3  23649  mdbr4  23650  ssmd1  23663  dmdsl3  23667  mdslmd1lem2  23678  mdslmd4i  23685  mdexchi  23687  atssma  23730  atoml2i  23735  chirredlem3  23744  mdsymlem1  23755  mdsymlem3  23757  dmdbr6ati  23775  dmdbr7ati  23776  cdjreui  23784  cdj3lem2b  23789  addltmulALT  23798  ssrmo  23826  iundifdif  23858  imadifxp  23882  fimacnvinrn2  23892  sspreima  23900  disjdsct  23932  xlt2addrd  23961  ressmulgnn0  24036  xrge0neqmnf  24042  xrge0nre  24043  kerunit  24078  mndpluscn  24117  rge0scvg  24140  pnfneige0  24141  indval2  24209  esumnul  24240  gsumesum  24248  esumcst  24252  pwsiga  24310  insiga  24317  elsigagen2  24328  measxun2  24359  aean  24390  mbfmfun  24399  mbfmbfm  24403  1stmbfm  24405  2ndmbfm  24406  dya2iocnrect  24426  probun  24457  dstfrvclim1  24515  coinfliprv  24520  ballotlem2  24526  ballotlemfp1  24529  ballotlemic  24544  ballotlem1c  24545  cvmliftlem10  24761  ghomgrpilem2  24877  prodf1  24999  fprodfac  25076  risefacp1  25114  fallfacp1  25115  faclim  25124  dfon2lem3  25166  dfon2lem7  25170  dfon2lem8  25171  rdgprc0  25175  wfrlem4  25284  wfrlem5  25285  wfrlem10  25290  wfrlem15  25295  frrlem4  25309  frrlem5  25310  unisnif  25489  funpartlem  25506  axcontlem7  25624  hfun  25834  df3nandALT1  25861  lukshef-ax2  25880  nandsym1  25887  ftc1cnnc  25980  trer  26011  clsun  26023  opnregcld  26025  cldregopn  26026  ssref  26055  fnessref  26065  fnopabco  26116  frinfm  26129  nninfnub  26147  caushft  26159  bndss  26187  ispridl2  26340  istopclsd  26446  pellex  26590  rmspecsqrnq  26661  monotoddzzfi  26697  jm2.23  26759  expdioph  26786  dford3lem1  26789  wopprc  26793  inisegn0  26810  kelac1  26831  dfac21  26834  lsmfgcl  26842  pwssplit4  26861  dsmmbas2  26873  isnumbasgrp  26942  dgraalem  27020  en1uniel  27050  psgnunilem4  27090  pm10.12  27223  pm11.61  27262  sbiota1  27304  fnchoice  27369  fmuldfeq  27382  infrglb  27391  climsuselem1  27402  climsuse  27403  stoweidlem28  27446  stoweidlem48  27466  stoweidlem52  27470  stoweidlem57  27475  wallispilem3  27485  wallispilem4  27486  wallispi  27488  wallispi2lem1  27489  wallispi2lem2  27490  wallispi2  27491  stirlinglem7  27498  stirlinglem10  27501  stirlinglem12  27503  dandysum2p2e4  27612  2reu4a  27636  ndmaovrcl  27738  frgra3v  27756  3vfriswmgra  27759  1to3vfriswmgra  27761  1to3vfriendship  27762  2pthfrgra  27765  4cycl2v2nb  27770  n4cyclfrgra  27772  frgranbnb  27774  frgrancvvdeqlem4  27786  frgrawopreg  27802  biimp  27911  bi2imp  27912  bi3impb  27913  bi3impa  27914  bi13impib  27916  bi123impib  27917  bi13impia  27918  bi123impia  27919  bi13imp23  27922  bi13imp2  27923  bi12imp3  27924  dfvd1imp  28009  dfvd2imp  28046  e1bi  28072  e2bi  28075  e3bi  28192  3ornot23VD  28301  3impexpbicomVD  28311  3impexpbicomiVD  28312  tratrbVD  28315  ssralv2VD  28320  equncomiVD  28323  truniALTVD  28332  ee33VD  28333  csbingVD  28338  onfrALTlem3VD  28341  onfrALTlem2VD  28343  onfrALTlem1VD  28344  onfrALTVD  28345  csbsngVD  28347  csbxpgVD  28348  csbrngVD  28350  csbunigVD  28352  csbfv12gALTVD  28353  relopabVD  28355  2uasbanhVD  28365  vk15.4jVD  28368  unisnALT  28380  chordthmALT  28388  bnj529  28448  bnj927  28478  bnj1379  28541  bnj1424  28549  bnj1436  28550  bnj1476  28557  bnj607  28626  bnj849  28635  bnj908  28641  bnj1097  28689  bnj1118  28692  bnj1128  28698  bnj1145  28701  bnj1154  28707  bnj1174  28711  bnj1189  28717  bnj1204  28720  bnj1279  28726  bnj1388  28741  bnj1417  28749  lubunNEW  29089  lkr0f  29210  glbconN  29492  paddssat  29929  pclunN  30013  2polssN  30030  paddunN  30042  poldmj1N  30043  ltrnnid  30251  dibglbN  31282
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