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

Theorem biimpi 186
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 178 . 2  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
31, 2ax-mp 8 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  sylbi  187  sylib  188  biimpri  197  mpbi  199  syl5bi  208  syl6ib  217  syl7bi  221  syl8ib  222  bitri  240  pm2.53  362  simplbi  446  simprbi  450  sylanb  458  sylan2b  461  pm3.1  484  orbi2i  505  pm2.32  512  anc2l  538  pm3.37  562  dfbi  610  pm2.76  821  pm5.15  859  pm5.16  860  pm5.75  903  rnlem  931  simp1bi  970  simp2bi  971  simp3bi  972  syl3an1b  1218  syl3an2b  1219  syl3an3b  1220  nic-ax  1428  19.25  1590  sbbii  1635  hbn1fw  1680  ax10-16  2131  exmoeu  2186  2mo  2222  eqeq1  2290  eleq2  2345  gencbvex  2831  moeq  2942  euind  2953  reuind  2969  eqsbc3r  3049  ssel  3175  unssd  3352  ssind  3394  n0moeu  3468  ss0  3486  uneqdifeq  3543  prprc  3739  ssunsn2  3774  eqsn  3776  trint  4129  snexALT  4195  snex  4215  pocl  4320  wefrc  4386  unexg  4520  unisn2  4521  reusv3i  4540  ordsson  4580  peano2  4675  brrelex12  4725  elrel  4788  dmxp  4896  xpssres  4988  elres  4989  elimasni  5039  dmsnsnsn  5149  coi2  5187  nfunv  5251  funun  5262  funcnv3  5277  funimass1  5291  funssxp  5368  f1o00  5474  dffv2  5554  fndmin  5594  iinpreima  5617  fsn2  5660  fnsuppeq0  5695  isoselem  5800  oprabid  5844  1stval  6086  2ndval  6087  1stdm  6129  exopxfr2  6146  oprabco  6165  poxp  6189  sorpsscmpl  6250  iotabi  6262  uniabio  6263  iotaint  6266  riotaxfrd  6332  tz7.49c  6454  undifixp  6848  bren2  6888  ensym  6906  domunsn  7007  limenpsi  7032  php4  7044  isinf  7072  en2  7090  findcard2  7094  unfilem1  7117  fissuni  7156  elfiun  7179  marypha1lem  7182  marypha2lem3  7186  supmaxlem  7211  brwdom2  7283  brwdom3  7292  preleq  7314  inf3lem2  7326  tcmin  7422  rankvalb  7465  prwf  7479  r1pw  7513  rankuni2b  7521  rankr1id  7530  cardval3  7581  ficardom  7590  cardmin2  7627  isinfcard  7715  iscard3  7716  alephval3  7733  dfac9  7758  kmlem6  7777  ackbij1lem12  7853  fin23lem29  7963  fin23lem30  7964  fin23lem41  7974  isf32lem11  7985  isfin1-3  8008  fin1a2lem11  8032  fin1a2lem12  8033  fin1a2lem13  8034  axcc2lem  8058  dominf  8067  axdc4lem  8077  dominfac  8191  pwcfsdom  8201  cfpwsdom  8202  tskuni  8401  wfgru  8434  rpregt0  10363  xrrebnd  10493  xaddf  10547  supxrun  10630  elfz1end  10816  fzennn  11026  cardfz  11028  ser0  11094  crreczi  11222  faclbnd  11299  bcn1  11321  hashssdif  11370  hashsnlei  11372  hashpw  11384  hashfun  11385  sqr0  11723  cau3lem  11834  harmonic  12313  mertenslem2  12337  rpnnen2  12500  prmind2  12765  pceq0  12919  prmreclem6  12964  0ram  13063  ram0  13065  ressbas2  13195  ressinbas  13200  mrcuni  13519  mreexexlem4d  13545  catpropd  13608  arwhoma  13873  lubun  14223  psssdm  14321  plusfeq  14377  gsum2d  15219  staffn  15610  scafeq  15643  lbsexg  15913  lidldvgen  16003  ply1bascl2  16281  prmirred  16444  zlmassa  16474  frgpcyg  16523  ipfeq  16550  isbasis3g  16683  isopn2  16765  ntrval2  16784  toponmre  16826  innei  16858  restcld  16899  restcldi  16900  discmp  17121  cmpsublem  17122  cmpsub  17123  2ndcctbss  17177  ptcnp  17312  kqf  17434  fbun  17531  opnfbas  17533  cfinfil  17584  supfil  17586  ufprim  17600  acufl  17608  filufint  17611  ufldom  17653  hausflf2  17689  alexsubALTlem4  17740  zlmclm  18589  cphassr  18643  ovolun  18854  volun  18898  dyadmax  18949  vitalilem2  18960  dvmptfsum  19318  rolle  19333  ulmcaulem  19767  logfac  19950  logno1  19979  logreclem  20112  leibpilem1  20232  prmorcht  20412  pclogsum  20450  2sqlem10  20609  chto1lb  20623  grpoidinvlem3  20867  nmlno0lem  21365  blocni  21377  pythi  21422  normpythi  21717  isch3  21817  shmodsi  21964  omlsilem  21977  pjchi  22007  chlubii  22047  osumi  22217  nmlnop0iALT  22571  nmopun  22590  cnlnssadj  22656  nmopcoi  22671  mdbr3  22873  mdbr4  22874  ssmd1  22887  dmdsl3  22891  mdslmd1lem2  22902  mdslmd4i  22909  mdexchi  22911  atssma  22954  atoml2i  22959  chirredlem3  22968  mdsymlem1  22979  mdsymlem3  22981  dmdbr6ati  22999  dmdbr7ati  23000  cdjreui  23008  cdj3lem2b  23013  addltmulALT  23022  ballotlem2  23043  ballotlemfp1  23046  ballotlemic  23061  ballotlem1c  23062  ballotlemro  23077  cvmliftlem10  23232  ghomgrpilem2  23400  dfon2lem3  23545  dfon2lem7  23549  dfon2lem8  23550  rdgprc0  23554  wfrlem4  23663  wfrlem5  23664  wfrlem10  23669  wfrlem15  23674  frrlem4  23688  frrlem5  23689  axfelem22  23771  unisnif  23874  axcontlem7  24008  hfun  24218  df3nandALT1  24245  lukshef-ax2  24264  nandsym1  24271  bibox  24392  binxt  24394  bidia  24399  splint  24458  twsymr  24488  imfstnrelc  24491  isfinite1b  24516  sssu  24552  prmapcp2  24568  supaub  24684  geme2  24686  toplat  24701  clfsebsr  24760  muldisc  24892  svli2  24895  intopcoaconb  24951  usptop  24961  limptlimpr2lem1  24985  limptlimpr2lem2  24986  islimrs  24991  flfneic  25035  supnufb  25041  dmrngcmp  25162  homib  25207  cmpmon  25226  idmon  25228  iepiclem  25234  idsubc  25262  idsubidsup  25268  idsubfun  25269  propsrc  25279  inttaror  25311  prismorcsetlemc  25328  domcatfun  25336  codcatfun  25345  idcatfun  25352  cmp2morpcats  25372  cmp2morpdom  25375  isconc2  25418  lineval4a  25498  isconcl6ab  25515  abhp  25584  trer  25638  clsun  25657  opnregcld  25659  cldregopn  25660  ssref  25694  fnessref  25704  fnopabco  25799  frinfm  25827  nninfnub  25872  caushft  25888  bndss  25921  ispridl2  26074  istopclsd  26186  pellex  26331  rmspecsqrnq  26402  monotoddzzfi  26438  jm2.23  26500  expdioph  26527  dford3lem1  26530  wopprc  26534  inisegn0  26551  kelac1  26572  dfac21  26575  lsmfgcl  26583  pwssplit4  26602  dsmmbas2  26614  isnumbasgrp  26683  dgraalem  26761  en1uniel  26791  psgnunilem4  26831  pm10.12  26964  pm11.61  27003  sbiota1  27045  fnchoice  27111  fmuldfeq  27124  infrglb  27133  climsuselem1  27144  climsuse  27145  stoweidlem16  27176  stoweidlem17  27177  stoweidlem20  27180  stoweidlem28  27188  stoweidlem31  27191  stoweidlem42  27202  stoweidlem48  27208  stoweidlem51  27211  stoweidlem52  27212  stoweidlem54  27214  stoweidlem57  27217  wallispilem3  27227  wallispilem4  27228  wallispi  27230  wallispi2lem1  27231  wallispi2lem2  27232  wallispi2  27233  stirlinglem7  27240  stirlinglem10  27243  stirlinglem12  27245  stirlinglem13  27246  aibandbiaiffaiffb  27253  aibandbiaiaiffb  27254  notatnand  27255  aistia  27256  aisfina  27257  bothfbothsame  27259  axorbtnotaiffb  27262  aiffnbandciffatnotciffb  27263  axorbciffatcxorb  27264  aibnbna  27265  aisbnaxb  27270  abnotbtaxb  27275  abnotataxb  27276  dandysum2p2e4  27334  2reu4a  27358  ndmaovrcl  27455  logbcl  27538  dfvd1imp  27627  dfvd2imp  27655  e1bi  27681  e2bi  27684  e3bi  27793  3ornot23VD  27903  3impexpbicomVD  27913  3impexpbicomiVD  27914  tratrbVD  27917  ssralv2VD  27922  equncomiVD  27925  truniALTVD  27934  ee33VD  27935  csbingVD  27940  onfrALTlem3VD  27943  onfrALTlem2VD  27945  onfrALTlem1VD  27946  onfrALTVD  27947  csbsngVD  27949  csbxpgVD  27950  csbrngVD  27952  csbunigVD  27954  csbfv12gALTVD  27955  relopabVD  27957  2uasbanhVD  27967  vk15.4jVD  27970  unisnALT  27982  bnj529  28049  bnj927  28079  bnj1379  28142  bnj1424  28150  bnj1436  28151  bnj1476  28158  bnj607  28227  bnj849  28236  bnj908  28242  bnj1097  28290  bnj1118  28293  bnj1128  28299  bnj1145  28302  bnj1154  28308  bnj1174  28312  bnj1189  28318  bnj1204  28321  bnj1279  28327  bnj1388  28342  bnj1417  28350  ax12OLD  28384  lubunNEW  28442  lkr0f  28563  glbconN  28845  paddssat  29282  pclunN  29366  2polssN  29383  paddunN  29395  poldmj1N  29396  ltrnnid  29604  dibglbN  30635
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 177
  Copyright terms: Public domain W3C validator