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  2224  exmoeu  2280  2mo  2316  eqeq1  2393  eleq2  2448  gencbvex  2941  moeq  3053  euind  3064  reuind  3080  eqsbc3r  3161  ssel  3285  unssd  3466  ssind  3508  n0moeu  3583  ss0  3601  uneqdifeq  3659  prprc  3859  ssunsn2  3901  eqsn  3903  trint  4258  snexALT  4326  snex  4346  pocl  4451  wefrc  4517  unexg  4650  unisn2  4651  reusv3i  4670  ordsson  4710  peano2  4805  brrelex12  4855  elrel  4918  dmxp  5028  xpssres  5120  elres  5121  elimasni  5171  dmsnsnsn  5288  coi2  5326  xpco  5354  iotabi  5367  uniabio  5368  iotaint  5371  nfunv  5424  funun  5435  funcnv3  5452  funimass1  5466  funssxp  5544  f1o00  5650  dffv3  5664  dffv2  5735  fndmin  5776  iinpreima  5799  fsn2  5847  ftpg  5855  fnsuppeq0  5892  isoselem  6000  oprabid  6044  1stval  6290  2ndval  6291  1stdm  6333  exopxfr2  6350  oprabco  6370  poxp  6394  sorpsscmpl  6469  riotaxfrd  6517  tz7.49c  6639  undifixp  7034  bren2  7074  ensym  7092  domunsn  7193  limenpsi  7218  php4  7230  isinf  7258  en2  7280  findcard2  7284  unfilem1  7307  fissuni  7346  elfiun  7370  marypha1lem  7373  marypha2lem3  7377  supmaxlem  7402  brwdom2  7474  brwdom3  7483  preleq  7505  inf3lem2  7517  tcmin  7613  rankvalb  7656  prwf  7670  r1pw  7704  rankuni2b  7712  rankr1id  7721  cardval3  7772  ficardom  7781  cardmin2  7818  isinfcard  7906  iscard3  7907  alephval3  7924  dfac9  7949  kmlem6  7968  ackbij1lem12  8044  fin23lem29  8154  fin23lem30  8155  fin23lem41  8165  isf32lem11  8176  isfin1-3  8199  fin1a2lem11  8223  fin1a2lem12  8224  fin1a2lem13  8225  axcc2lem  8249  dominf  8258  axdc4lem  8268  dominfac  8381  pwcfsdom  8391  cfpwsdom  8392  tskuni  8591  wfgru  8624  rpregt0  10557  xrrebnd  10688  xaddf  10742  supxrun  10826  elfz1end  11013  1fv  11050  elfznelfzob  11120  fzennn  11234  cardfz  11236  ser0  11302  crreczi  11431  faclbnd  11508  bcn1  11531  hashinfxadd  11586  hashge0  11588  hashssdif  11604  hashsnlei  11607  hashpw  11626  hashfun  11627  s4f1o  11792  sqr0  11974  cau3lem  12085  harmonic  12565  mertenslem2  12589  rpnnen2  12752  prmind2  13017  pceq0  13171  prmreclem6  13216  0ram  13315  ram0  13317  ressbas2  13447  ressinbas  13452  mrcuni  13773  mreexexlem4d  13799  catpropd  13862  arwhoma  14127  lubun  14477  psssdm  14575  plusfeq  14631  gsum2d  15473  staffn  15864  scafeq  15897  lbsexg  16163  lidldvgen  16253  ply1bascl2  16529  prmirred  16698  zlmassa  16728  frgpcyg  16777  ipfeq  16804  isbasis3g  16937  isopn2  17019  ntrval2  17038  toponmre  17080  innei  17112  restcld  17158  restcldi  17159  neitr  17166  discmp  17383  cmpsublem  17384  cmpsub  17385  2ndcctbss  17439  ptcnp  17575  imasnopn  17643  imasncld  17644  imasncls  17645  kqf  17700  fbun  17793  opnfbas  17795  cfinfil  17846  supfil  17848  ufprim  17862  acufl  17870  filufint  17873  ufldom  17915  hausflf2  17951  alexsubALTlem4  18002  cnextfval  18014  cnextfun  18016  cnextfres  18020  trust  18180  utoptop  18185  ustuqtop1  18192  metustid  18474  metustfbas  18477  cfilucfil  18479  metustbl  18486  restmetu  18489  zlmclm  18991  cphassr  19045  ovolun  19262  volun  19306  dyadmax  19357  vitalilem2  19368  dvmptfsum  19726  rolle  19741  ulmcaulem  20177  logfac  20362  logno1  20394  logreclem  20527  leibpilem1  20647  prmorcht  20828  pclogsum  20866  2sqlem10  21025  chto1lb  21039  ausisusgra  21247  usgra2edg1  21269  usgrarnedg  21270  usgraedg4  21272  usgra1v  21275  usgraidx2vlem2  21277  usgraidx2v  21278  usgrares1  21290  nb3graprlem2  21327  nb3grapr  21328  nb3grapr2  21329  nb3gra2nb  21330  cusgra3v  21339  cusgrafilem2  21355  usgrasscusgra  21358  uvtxnbgra  21368  constr1trl  21436  constr2trl  21446  fargshiftfo  21473  vdgrnn0pnf  21528  eupatrl  21538  grpoidinvlem3  21642  nmlno0lem  22142  blocni  22154  pythi  22199  normpythi  22492  isch3  22592  shmodsi  22739  omlsilem  22752  pjchi  22782  chlubii  22822  osumi  22992  nmlnop0iALT  23346  nmopun  23365  cnlnssadj  23431  nmopcoi  23446  mdbr3  23648  mdbr4  23649  ssmd1  23662  dmdsl3  23666  mdslmd1lem2  23677  mdslmd4i  23684  mdexchi  23686  atssma  23729  atoml2i  23734  chirredlem3  23743  mdsymlem1  23754  mdsymlem3  23756  dmdbr6ati  23774  dmdbr7ati  23775  cdjreui  23783  cdj3lem2b  23788  addltmulALT  23797  ssrmo  23825  iundifdif  23857  imadifxp  23881  fimacnvinrn2  23891  sspreima  23899  disjdsct  23931  xlt2addrd  23960  ressmulgnn0  24035  xrge0neqmnf  24041  xrge0nre  24042  kerunit  24077  mndpluscn  24116  rge0scvg  24139  pnfneige0  24140  indval2  24208  esumnul  24239  gsumesum  24247  esumcst  24251  pwsiga  24309  insiga  24316  elsigagen2  24327  measxun2  24358  aean  24389  mbfmfun  24398  mbfmbfm  24402  1stmbfm  24404  2ndmbfm  24405  dya2iocnrect  24425  probun  24456  dstfrvclim1  24514  coinfliprv  24519  ballotlem2  24525  ballotlemfp1  24528  ballotlemic  24543  ballotlem1c  24544  cvmliftlem10  24760  ghomgrpilem2  24876  prodf1  24998  fprodfac  25075  risefacp1  25113  fallfacp1  25114  faclim  25123  dfon2lem3  25165  dfon2lem7  25169  dfon2lem8  25170  rdgprc0  25174  wfrlem4  25283  wfrlem5  25284  wfrlem10  25289  wfrlem15  25294  frrlem4  25308  frrlem5  25309  unisnif  25488  funpartlem  25505  axcontlem7  25623  hfun  25833  df3nandALT1  25860  lukshef-ax2  25879  nandsym1  25886  ftc1cnnc  25979  trer  26010  clsun  26022  opnregcld  26024  cldregopn  26025  ssref  26054  fnessref  26064  fnopabco  26115  frinfm  26128  nninfnub  26146  caushft  26158  bndss  26186  ispridl2  26339  istopclsd  26445  pellex  26589  rmspecsqrnq  26660  monotoddzzfi  26696  jm2.23  26758  expdioph  26785  dford3lem1  26788  wopprc  26792  inisegn0  26809  kelac1  26830  dfac21  26833  lsmfgcl  26841  pwssplit4  26860  dsmmbas2  26872  isnumbasgrp  26941  dgraalem  27019  en1uniel  27049  psgnunilem4  27089  pm10.12  27222  pm11.61  27261  sbiota1  27303  fnchoice  27368  fmuldfeq  27381  infrglb  27390  climsuselem1  27401  climsuse  27402  stoweidlem28  27445  stoweidlem48  27465  stoweidlem52  27469  stoweidlem57  27474  wallispilem3  27484  wallispilem4  27485  wallispi  27487  wallispi2lem1  27488  wallispi2lem2  27489  wallispi2  27490  stirlinglem7  27497  stirlinglem10  27500  stirlinglem12  27502  dandysum2p2e4  27611  2reu4a  27635  ndmaovrcl  27737  frgra3v  27755  3vfriswmgra  27758  1to3vfriswmgra  27760  1to3vfriendship  27761  2pthfrgra  27764  4cycl2v2nb  27769  n4cyclfrgra  27771  frgranbnb  27773  frgrancvvdeqlem4  27785  frgrawopreg  27801  biimp  27910  bi2imp  27911  bi3impb  27912  bi3impa  27913  bi13impib  27915  bi123impib  27916  bi13impia  27917  bi123impia  27918  bi13imp23  27921  bi13imp2  27922  bi12imp3  27923  dfvd1imp  28008  dfvd2imp  28045  e1bi  28071  e2bi  28074  e3bi  28191  3ornot23VD  28300  3impexpbicomVD  28310  3impexpbicomiVD  28311  tratrbVD  28314  ssralv2VD  28319  equncomiVD  28322  truniALTVD  28331  ee33VD  28332  csbingVD  28337  onfrALTlem3VD  28340  onfrALTlem2VD  28342  onfrALTlem1VD  28343  onfrALTVD  28344  csbsngVD  28346  csbxpgVD  28347  csbrngVD  28349  csbunigVD  28351  csbfv12gALTVD  28352  relopabVD  28354  2uasbanhVD  28364  vk15.4jVD  28367  unisnALT  28379  chordthmALT  28387  bnj529  28447  bnj927  28477  bnj1379  28540  bnj1424  28548  bnj1436  28549  bnj1476  28556  bnj607  28625  bnj849  28634  bnj908  28640  bnj1097  28688  bnj1118  28691  bnj1128  28697  bnj1145  28700  bnj1154  28706  bnj1174  28710  bnj1189  28716  bnj1204  28719  bnj1279  28725  bnj1388  28740  bnj1417  28748  lubunNEW  29088  lkr0f  29209  glbconN  29491  paddssat  29928  pclunN  30012  2polssN  30029  paddunN  30041  poldmj1N  30042  ltrnnid  30250  dibglbN  31281
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