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  24212  dfon2lem7  24216  dfon2lem8  24217  rdgprc0  24221  wfrlem4  24330  wfrlem5  24331  wfrlem10  24336  wfrlem15  24341  frrlem4  24355  frrlem5  24356  unisnif  24535  funpartlem  24552  axcontlem7  24670  hfun  24880  df3nandALT1  24907  lukshef-ax2  24926  nandsym1  24933  ftc1cnnc  25025  bibox  25085  binxt  25087  bidia  25092  splint  25151  twsymr  25181  imfstnrelc  25184  isfinite1b  25209  sssu  25244  prmapcp2  25260  supaub  25376  geme2  25378  toplat  25393  clfsebsr  25452  muldisc  25584  svli2  25587  intopcoaconb  25643  usptop  25653  limptlimpr2lem1  25677  limptlimpr2lem2  25678  islimrs  25683  flfneic  25727  supnufb  25733  dmrngcmp  25854  homib  25899  cmpmon  25918  idmon  25920  iepiclem  25926  idsubc  25954  idsubidsup  25960  idsubfun  25961  propsrc  25971  inttaror  26003  prismorcsetlemc  26020  domcatfun  26028  codcatfun  26037  idcatfun  26044  cmp2morpcats  26064  cmp2morpdom  26067  isconc2  26110  lineval4a  26190  isconcl6ab  26207  abhp  26276  trer  26330  clsun  26349  opnregcld  26351  cldregopn  26352  ssref  26386  fnessref  26396  fnopabco  26491  frinfm  26519  nninfnub  26564  caushft  26580  bndss  26613  ispridl2  26766  istopclsd  26878  pellex  27023  rmspecsqrnq  27094  monotoddzzfi  27130  jm2.23  27192  expdioph  27219  dford3lem1  27222  wopprc  27226  inisegn0  27243  kelac1  27264  dfac21  27267  lsmfgcl  27275  pwssplit4  27294  dsmmbas2  27306  isnumbasgrp  27375  dgraalem  27453  en1uniel  27483  psgnunilem4  27523  pm10.12  27656  pm11.61  27695  sbiota1  27737  fnchoice  27803  fmuldfeq  27816  infrglb  27825  climsuselem1  27836  climsuse  27837  stoweidlem16  27868  stoweidlem17  27869  stoweidlem20  27872  stoweidlem28  27880  stoweidlem31  27883  stoweidlem42  27894  stoweidlem48  27900  stoweidlem51  27903  stoweidlem52  27904  stoweidlem54  27906  stoweidlem57  27909  wallispilem3  27919  wallispilem4  27920  wallispi  27922  wallispi2lem1  27923  wallispi2lem2  27924  wallispi2  27925  stirlinglem7  27932  stirlinglem10  27935  stirlinglem12  27937  stirlinglem13  27938  aibandbiaiffaiffb  27965  aibandbiaiaiffb  27966  notatnand  27967  aistia  27968  aisfina  27969  bothfbothsame  27971  axorbtnotaiffb  27974  aiffnbandciffatnotciffb  27975  axorbciffatcxorb  27976  aibnbna  27977  aisbnaxb  27982  abnotbtaxb  27987  abnotataxb  27988  dandysum2p2e4  28046  2reu4a  28070  ndmaovrcl  28172  s4f1o  28225  usgra1v  28260  nb3graprlem2  28288  nb3grapr  28289  nb3grapr2  28290  nb3gra2nb  28291  nbcusgra  28298  cusgra3v  28299  uvtxnbgra  28306  fargshiftfo  28383  eupatrl  28385  frgra3v  28426  3vfriswmgra  28429  1to3vfriswmgra  28431  1to3vfriendship  28432  4cycl2v2nb  28438  n4cyclfrgra  28440  biimp  28545  bi2imp  28546  bi3impb  28547  bi3impa  28548  bi13impib  28550  bi123impib  28551  bi13impia  28552  bi123impia  28553  bi13imp2  28557  bi12imp3  28558  dfvd1imp  28643  dfvd2imp  28680  e1bi  28706  e2bi  28709  e3bi  28827  3ornot23VD  28939  3impexpbicomVD  28949  3impexpbicomiVD  28950  tratrbVD  28953  ssralv2VD  28958  equncomiVD  28961  truniALTVD  28970  ee33VD  28971  csbingVD  28976  onfrALTlem3VD  28979  onfrALTlem2VD  28981  onfrALTlem1VD  28982  onfrALTVD  28983  csbsngVD  28985  csbxpgVD  28986  csbrngVD  28988  csbunigVD  28990  csbfv12gALTVD  28991  relopabVD  28993  2uasbanhVD  29003  vk15.4jVD  29006  unisnALT  29018  chordthmALT  29026  bnj529  29086  bnj927  29116  bnj1379  29179  bnj1424  29187  bnj1436  29188  bnj1476  29195  bnj607  29264  bnj849  29273  bnj908  29279  bnj1097  29327  bnj1118  29330  bnj1128  29336  bnj1145  29339  bnj1154  29345  bnj1174  29349  bnj1189  29355  bnj1204  29358  bnj1279  29364  bnj1388  29379  bnj1417  29387  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