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  1593  sbbii  1643  spvw  1655  hbn1fw  1691  ax10-16  2142  exmoeu  2198  2mo  2234  eqeq1  2302  eleq2  2357  gencbvex  2843  moeq  2954  euind  2965  reuind  2981  eqsbc3r  3061  ssel  3187  unssd  3364  ssind  3406  n0moeu  3480  ss0  3498  uneqdifeq  3555  prprc  3751  ssunsn2  3789  eqsn  3791  trint  4144  snexALT  4212  snex  4232  pocl  4337  wefrc  4403  unexg  4537  unisn2  4538  reusv3i  4557  ordsson  4597  peano2  4692  brrelex12  4742  elrel  4805  dmxp  4913  xpssres  5005  elres  5006  elimasni  5056  dmsnsnsn  5167  coi2  5205  iotabi  5244  uniabio  5245  iotaint  5248  nfunv  5301  funun  5312  funcnv3  5327  funimass1  5341  funssxp  5418  f1o00  5524  dffv3  5537  dffv2  5608  fndmin  5648  iinpreima  5671  fsn2  5714  fnsuppeq0  5749  isoselem  5854  oprabid  5898  1stval  6140  2ndval  6141  1stdm  6183  exopxfr2  6200  oprabco  6219  poxp  6243  sorpsscmpl  6304  riotaxfrd  6352  tz7.49c  6474  undifixp  6868  bren2  6908  ensym  6926  domunsn  7027  limenpsi  7052  php4  7064  isinf  7092  en2  7110  findcard2  7114  unfilem1  7137  fissuni  7176  elfiun  7199  marypha1lem  7202  marypha2lem3  7206  supmaxlem  7231  brwdom2  7303  brwdom3  7312  preleq  7334  inf3lem2  7346  tcmin  7442  rankvalb  7485  prwf  7499  r1pw  7533  rankuni2b  7541  rankr1id  7550  cardval3  7601  ficardom  7610  cardmin2  7647  isinfcard  7735  iscard3  7736  alephval3  7753  dfac9  7778  kmlem6  7797  ackbij1lem12  7873  fin23lem29  7983  fin23lem30  7984  fin23lem41  7994  isf32lem11  8005  isfin1-3  8028  fin1a2lem11  8052  fin1a2lem12  8053  fin1a2lem13  8054  axcc2lem  8078  dominf  8087  axdc4lem  8097  dominfac  8211  pwcfsdom  8221  cfpwsdom  8222  tskuni  8421  wfgru  8454  rpregt0  10383  xrrebnd  10513  xaddf  10567  supxrun  10650  elfz1end  10836  fzennn  11046  cardfz  11048  ser0  11114  crreczi  11242  faclbnd  11319  bcn1  11341  hashssdif  11390  hashsnlei  11392  hashpw  11404  hashfun  11405  sqr0  11743  cau3lem  11854  harmonic  12333  mertenslem2  12357  rpnnen2  12520  prmind2  12785  pceq0  12939  prmreclem6  12984  0ram  13083  ram0  13085  ressbas2  13215  ressinbas  13220  mrcuni  13539  mreexexlem4d  13565  catpropd  13628  arwhoma  13893  lubun  14243  psssdm  14341  plusfeq  14397  gsum2d  15239  staffn  15630  scafeq  15663  lbsexg  15933  lidldvgen  16023  ply1bascl2  16301  prmirred  16464  zlmassa  16494  frgpcyg  16543  ipfeq  16570  isbasis3g  16703  isopn2  16785  ntrval2  16804  toponmre  16846  innei  16878  restcld  16919  restcldi  16920  discmp  17141  cmpsublem  17142  cmpsub  17143  2ndcctbss  17197  ptcnp  17332  kqf  17454  fbun  17551  opnfbas  17553  cfinfil  17604  supfil  17606  ufprim  17620  acufl  17628  filufint  17631  ufldom  17673  hausflf2  17709  alexsubALTlem4  17760  zlmclm  18609  cphassr  18663  ovolun  18874  volun  18918  dyadmax  18969  vitalilem2  18980  dvmptfsum  19338  rolle  19353  ulmcaulem  19787  logfac  19970  logno1  19999  logreclem  20132  leibpilem1  20252  prmorcht  20432  pclogsum  20470  2sqlem10  20629  chto1lb  20643  grpoidinvlem3  20889  nmlno0lem  21387  blocni  21399  pythi  21444  normpythi  21737  isch3  21837  shmodsi  21984  omlsilem  21997  pjchi  22027  chlubii  22067  osumi  22237  nmlnop0iALT  22591  nmopun  22610  cnlnssadj  22676  nmopcoi  22691  mdbr3  22893  mdbr4  22894  ssmd1  22907  dmdsl3  22911  mdslmd1lem2  22922  mdslmd4i  22929  mdexchi  22931  atssma  22974  atoml2i  22979  chirredlem3  22988  mdsymlem1  22999  mdsymlem3  23001  dmdbr6ati  23019  dmdbr7ati  23020  cdjreui  23028  cdj3lem2b  23033  addltmulALT  23042  ballotlem2  23063  ballotlemfp1  23066  ballotlemic  23081  ballotlem1c  23082  ballotlemro  23097  ssrmo  23164  elim2ifim  23169  iundifdifd  23175  iundifdif  23176  fimacnvinrn2  23215  sspreima  23225  xlt2addrd  23268  mndpluscn  23314  ressmulgnn0  23324  xrge0iifhom  23334  xrge0neqmnf  23345  disjdsct  23384  rge0scvg  23388  pnfneige0  23389  hashge0  23401  logbcl  23414  esumnul  23442  esumcst  23451  esumsn  23452  esumpinfval  23456  pwsiga  23506  insiga  23513  elsigagen2  23524  measxun2  23553  measssd  23558  mbfmfun  23574  mbfmbfm  23578  1stmbfm  23580  2ndmbfm  23581  indval2  23613  probun  23637  totprobd  23644  dstfrvclim1  23693  coinfliprv  23698  cvmliftlem10  23840  ghomgrpilem2  24008  faclimlem3  24119  faclimlem7  24123  prodf1  24165  dfon2lem3  24211  dfon2lem7  24215  dfon2lem8  24216  rdgprc0  24220  wfrlem4  24329  wfrlem5  24330  wfrlem10  24335  wfrlem15  24340  frrlem4  24354  frrlem5  24355  unisnif  24534  funpartlem  24551  axcontlem7  24669  hfun  24879  df3nandALT1  24906  lukshef-ax2  24925  nandsym1  24932  ftc1cnnc  25024  bibox  25084  binxt  25086  bidia  25091  splint  25150  twsymr  25180  imfstnrelc  25183  isfinite1b  25208  sssu  25243  prmapcp2  25259  supaub  25375  geme2  25377  toplat  25392  clfsebsr  25451  muldisc  25583  svli2  25586  intopcoaconb  25642  usptop  25652  limptlimpr2lem1  25676  limptlimpr2lem2  25677  islimrs  25682  flfneic  25726  supnufb  25732  dmrngcmp  25853  homib  25898  cmpmon  25917  idmon  25919  iepiclem  25925  idsubc  25953  idsubidsup  25959  idsubfun  25960  propsrc  25970  inttaror  26002  prismorcsetlemc  26019  domcatfun  26027  codcatfun  26036  idcatfun  26043  cmp2morpcats  26063  cmp2morpdom  26066  isconc2  26109  lineval4a  26189  isconcl6ab  26206  abhp  26275  trer  26329  clsun  26348  opnregcld  26350  cldregopn  26351  ssref  26385  fnessref  26395  fnopabco  26490  frinfm  26518  nninfnub  26563  caushft  26579  bndss  26612  ispridl2  26765  istopclsd  26877  pellex  27022  rmspecsqrnq  27093  monotoddzzfi  27129  jm2.23  27191  expdioph  27218  dford3lem1  27221  wopprc  27225  inisegn0  27242  kelac1  27263  dfac21  27266  lsmfgcl  27274  pwssplit4  27293  dsmmbas2  27305  isnumbasgrp  27374  dgraalem  27452  en1uniel  27482  psgnunilem4  27522  pm10.12  27655  pm11.61  27694  sbiota1  27736  fnchoice  27802  fmuldfeq  27815  infrglb  27824  climsuselem1  27835  climsuse  27836  stoweidlem16  27867  stoweidlem17  27868  stoweidlem20  27871  stoweidlem28  27879  stoweidlem31  27882  stoweidlem42  27893  stoweidlem48  27899  stoweidlem51  27902  stoweidlem52  27903  stoweidlem54  27905  stoweidlem57  27908  wallispilem3  27918  wallispilem4  27919  wallispi  27921  wallispi2lem1  27922  wallispi2lem2  27923  wallispi2  27924  stirlinglem7  27931  stirlinglem10  27934  stirlinglem12  27936  stirlinglem13  27937  aibandbiaiffaiffb  27964  aibandbiaiaiffb  27965  notatnand  27966  aistia  27967  aisfina  27968  bothfbothsame  27970  axorbtnotaiffb  27973  aiffnbandciffatnotciffb  27974  axorbciffatcxorb  27975  aibnbna  27976  aisbnaxb  27981  abnotbtaxb  27986  abnotataxb  27987  dandysum2p2e4  28045  2reu4a  28069  ndmaovrcl  28171  s4f1o  28224  usgra1v  28259  nb3graprlem2  28287  nb3grapr  28288  nb3grapr2  28289  nb3gra2nb  28290  nbcusgra  28297  cusgra3v  28298  uvtxnbgra  28305  fargshiftfo  28382  eupatrl  28384  frgra3v  28425  3vfriswmgra  28428  1to3vfriswmgra  28430  1to3vfriendship  28431  4cycl2v2nb  28437  n4cyclfrgra  28439  biimp  28544  bi2imp  28545  bi3impb  28546  bi3impa  28547  bi13impib  28549  bi123impib  28550  bi13impia  28551  bi123impia  28552  bi13imp2  28556  bi12imp3  28557  dfvd1imp  28642  dfvd2imp  28679  e1bi  28705  e2bi  28708  e3bi  28826  3ornot23VD  28938  3impexpbicomVD  28948  3impexpbicomiVD  28949  tratrbVD  28952  ssralv2VD  28957  equncomiVD  28960  truniALTVD  28969  ee33VD  28970  csbingVD  28975  onfrALTlem3VD  28978  onfrALTlem2VD  28980  onfrALTlem1VD  28981  onfrALTVD  28982  csbsngVD  28984  csbxpgVD  28985  csbrngVD  28987  csbunigVD  28989  csbfv12gALTVD  28990  relopabVD  28992  2uasbanhVD  29002  vk15.4jVD  29005  unisnALT  29017  chordthmALT  29025  bnj529  29085  bnj927  29115  bnj1379  29178  bnj1424  29186  bnj1436  29187  bnj1476  29194  bnj607  29263  bnj849  29272  bnj908  29278  bnj1097  29326  bnj1118  29329  bnj1128  29335  bnj1145  29338  bnj1154  29344  bnj1174  29348  bnj1189  29354  bnj1204  29357  bnj1279  29363  bnj1388  29378  bnj1417  29386  ax12OLD  29727  lubunNEW  29785  lkr0f  29906  glbconN  30188  paddssat  30625  pclunN  30709  2polssN  30726  paddunN  30738  poldmj1N  30739  ltrnnid  30947  dibglbN  31978
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