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  1592  sbbii  1636  hbn1fw  1681  ax10-16  2131  exmoeu  2187  2mo  2223  eqeq1  2291  eleq2  2346  gencbvex  2832  moeq  2943  euind  2954  reuind  2970  eqsbc3r  3050  ssel  3176  unssd  3353  ssind  3395  n0moeu  3469  ss0  3487  uneqdifeq  3544  prprc  3740  ssunsn2  3775  eqsn  3777  trint  4130  snexALT  4198  snex  4218  pocl  4323  wefrc  4389  unexg  4523  unisn2  4524  reusv3i  4543  ordsson  4583  peano2  4678  brrelex12  4728  elrel  4791  dmxp  4899  xpssres  4991  elres  4992  elimasni  5042  dmsnsnsn  5153  coi2  5191  iotabi  5230  uniabio  5231  iotaint  5234  nfunv  5287  funun  5298  funcnv3  5313  funimass1  5327  funssxp  5404  f1o00  5510  dffv3  5523  dffv2  5594  fndmin  5634  iinpreima  5657  fsn2  5700  fnsuppeq0  5735  isoselem  5840  oprabid  5884  1stval  6126  2ndval  6127  1stdm  6169  exopxfr2  6186  oprabco  6205  poxp  6229  sorpsscmpl  6290  riotaxfrd  6338  tz7.49c  6460  undifixp  6854  bren2  6894  ensym  6912  domunsn  7013  limenpsi  7038  php4  7050  isinf  7078  en2  7096  findcard2  7100  unfilem1  7123  fissuni  7162  elfiun  7185  marypha1lem  7188  marypha2lem3  7192  supmaxlem  7217  brwdom2  7289  brwdom3  7298  preleq  7320  inf3lem2  7332  tcmin  7428  rankvalb  7471  prwf  7485  r1pw  7519  rankuni2b  7527  rankr1id  7536  cardval3  7587  ficardom  7596  cardmin2  7633  isinfcard  7721  iscard3  7722  alephval3  7739  dfac9  7764  kmlem6  7783  ackbij1lem12  7859  fin23lem29  7969  fin23lem30  7970  fin23lem41  7980  isf32lem11  7991  isfin1-3  8014  fin1a2lem11  8038  fin1a2lem12  8039  fin1a2lem13  8040  axcc2lem  8064  dominf  8073  axdc4lem  8083  dominfac  8197  pwcfsdom  8207  cfpwsdom  8208  tskuni  8407  wfgru  8440  rpregt0  10369  xrrebnd  10499  xaddf  10553  supxrun  10636  elfz1end  10822  fzennn  11032  cardfz  11034  ser0  11100  crreczi  11228  faclbnd  11305  bcn1  11327  hashssdif  11376  hashsnlei  11378  hashpw  11390  hashfun  11391  sqr0  11729  cau3lem  11840  harmonic  12319  mertenslem2  12343  rpnnen2  12506  prmind2  12771  pceq0  12925  prmreclem6  12970  0ram  13069  ram0  13071  ressbas2  13201  ressinbas  13206  mrcuni  13525  mreexexlem4d  13551  catpropd  13614  arwhoma  13879  lubun  14229  psssdm  14327  plusfeq  14383  gsum2d  15225  staffn  15616  scafeq  15649  lbsexg  15919  lidldvgen  16009  ply1bascl2  16287  prmirred  16450  zlmassa  16480  frgpcyg  16529  ipfeq  16556  isbasis3g  16689  isopn2  16771  ntrval2  16790  toponmre  16832  innei  16864  restcld  16905  restcldi  16906  discmp  17127  cmpsublem  17128  cmpsub  17129  2ndcctbss  17183  ptcnp  17318  kqf  17440  fbun  17537  opnfbas  17539  cfinfil  17590  supfil  17592  ufprim  17606  acufl  17614  filufint  17617  ufldom  17659  hausflf2  17695  alexsubALTlem4  17746  zlmclm  18595  cphassr  18649  ovolun  18860  volun  18904  dyadmax  18955  vitalilem2  18966  dvmptfsum  19324  rolle  19339  ulmcaulem  19773  logfac  19956  logno1  19985  logreclem  20118  leibpilem1  20238  prmorcht  20418  pclogsum  20456  2sqlem10  20615  chto1lb  20629  grpoidinvlem3  20875  nmlno0lem  21373  blocni  21385  pythi  21430  normpythi  21723  isch3  21823  shmodsi  21970  omlsilem  21983  pjchi  22013  chlubii  22053  osumi  22223  nmlnop0iALT  22577  nmopun  22596  cnlnssadj  22662  nmopcoi  22677  mdbr3  22879  mdbr4  22880  ssmd1  22893  dmdsl3  22897  mdslmd1lem2  22908  mdslmd4i  22915  mdexchi  22917  atssma  22960  atoml2i  22965  chirredlem3  22974  mdsymlem1  22985  mdsymlem3  22987  dmdbr6ati  23005  dmdbr7ati  23006  cdjreui  23014  cdj3lem2b  23019  addltmulALT  23028  ballotlem2  23049  ballotlemfp1  23052  ballotlemic  23067  ballotlem1c  23068  ballotlemro  23083  ssrmo  23150  elim2ifim  23155  iundifdifd  23161  iundifdif  23162  fimacnvinrn2  23202  sspreima  23212  xlt2addrd  23255  mndpluscn  23301  ressmulgnn0  23311  xrge0iifhom  23321  xrge0neqmnf  23332  disjdsct  23371  rge0scvg  23375  pnfneige0  23376  hashge0  23388  logbcl  23401  esumnul  23429  esumcst  23438  esumsn  23439  esumpinfval  23443  pwsiga  23493  insiga  23500  elsigagen2  23511  measxun2  23540  measssd  23545  mbfmfun  23561  mbfmbfm  23565  1stmbfm  23567  2ndmbfm  23568  indval2  23600  probun  23624  totprobd  23631  dstfrvclim1  23680  coinfliprv  23685  cvmliftlem10  23827  ghomgrpilem2  23995  dfon2lem3  24143  dfon2lem7  24147  dfon2lem8  24148  rdgprc0  24152  wfrlem4  24261  wfrlem5  24262  wfrlem10  24267  wfrlem15  24272  frrlem4  24286  frrlem5  24287  unisnif  24466  axcontlem7  24600  hfun  24810  df3nandALT1  24837  lukshef-ax2  24856  nandsym1  24863  bibox  24993  binxt  24995  bidia  25000  splint  25059  twsymr  25089  imfstnrelc  25092  isfinite1b  25117  sssu  25152  prmapcp2  25168  supaub  25284  geme2  25286  toplat  25301  clfsebsr  25360  muldisc  25492  svli2  25495  intopcoaconb  25551  usptop  25561  limptlimpr2lem1  25585  limptlimpr2lem2  25586  islimrs  25591  flfneic  25635  supnufb  25641  dmrngcmp  25762  homib  25807  cmpmon  25826  idmon  25828  iepiclem  25834  idsubc  25862  idsubidsup  25868  idsubfun  25869  propsrc  25879  inttaror  25911  prismorcsetlemc  25928  domcatfun  25936  codcatfun  25945  idcatfun  25952  cmp2morpcats  25972  cmp2morpdom  25975  isconc2  26018  lineval4a  26098  isconcl6ab  26115  abhp  26184  trer  26238  clsun  26257  opnregcld  26259  cldregopn  26260  ssref  26294  fnessref  26304  fnopabco  26399  frinfm  26427  nninfnub  26472  caushft  26488  bndss  26521  ispridl2  26674  istopclsd  26786  pellex  26931  rmspecsqrnq  27002  monotoddzzfi  27038  jm2.23  27100  expdioph  27127  dford3lem1  27130  wopprc  27134  inisegn0  27151  kelac1  27172  dfac21  27175  lsmfgcl  27183  pwssplit4  27202  dsmmbas2  27214  isnumbasgrp  27283  dgraalem  27361  en1uniel  27391  psgnunilem4  27431  pm10.12  27564  pm11.61  27603  sbiota1  27645  fnchoice  27711  fmuldfeq  27724  infrglb  27733  climsuselem1  27744  climsuse  27745  stoweidlem16  27776  stoweidlem17  27777  stoweidlem20  27780  stoweidlem28  27788  stoweidlem31  27791  stoweidlem42  27802  stoweidlem48  27808  stoweidlem51  27811  stoweidlem52  27812  stoweidlem54  27814  stoweidlem57  27817  wallispilem3  27827  wallispilem4  27828  wallispi  27830  wallispi2lem1  27831  wallispi2lem2  27832  wallispi2  27833  stirlinglem7  27840  stirlinglem10  27843  stirlinglem12  27845  stirlinglem13  27846  aibandbiaiffaiffb  27873  aibandbiaiaiffb  27874  notatnand  27875  aistia  27876  aisfina  27877  bothfbothsame  27879  axorbtnotaiffb  27882  aiffnbandciffatnotciffb  27883  axorbciffatcxorb  27884  aibnbna  27885  aisbnaxb  27890  abnotbtaxb  27895  abnotataxb  27896  dandysum2p2e4  27954  2reu4a  27978  ndmaovrcl  28075  s4f1o  28104  usgra1v  28137  nbcusgra  28170  uvtxnbgra  28176  frgra3v  28191  3vfriswmgra  28194  1to3vfriswmgra  28196  1to3vfriendship  28197  biimp  28302  bi2imp  28303  bi3impb  28304  bi3impa  28305  bi13impib  28307  bi123impib  28308  bi13impia  28309  bi123impia  28310  bi13imp2  28314  bi12imp3  28315  dfvd1imp  28400  dfvd2imp  28437  e1bi  28463  e2bi  28466  e3bi  28584  3ornot23VD  28696  3impexpbicomVD  28706  3impexpbicomiVD  28707  tratrbVD  28710  ssralv2VD  28715  equncomiVD  28718  truniALTVD  28727  ee33VD  28728  csbingVD  28733  onfrALTlem3VD  28736  onfrALTlem2VD  28738  onfrALTlem1VD  28739  onfrALTVD  28740  csbsngVD  28742  csbxpgVD  28743  csbrngVD  28745  csbunigVD  28747  csbfv12gALTVD  28748  relopabVD  28750  2uasbanhVD  28760  vk15.4jVD  28763  unisnALT  28775  chordthmALT  28783  bnj529  28843  bnj927  28873  bnj1379  28936  bnj1424  28944  bnj1436  28945  bnj1476  28952  bnj607  29021  bnj849  29030  bnj908  29036  bnj1097  29084  bnj1118  29087  bnj1128  29093  bnj1145  29096  bnj1154  29102  bnj1174  29106  bnj1189  29112  bnj1204  29115  bnj1279  29121  bnj1388  29136  bnj1417  29144  ax12OLD  29178  lubunNEW  29236  lkr0f  29357  glbconN  29639  paddssat  30076  pclunN  30160  2polssN  30177  paddunN  30189  poldmj1N  30190  ltrnnid  30398  dibglbN  31429
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