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

Theorem impbii 181
Description: Infer an equivalence from an implication and its converse. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
impbii.1  |-  ( ph  ->  ps )
impbii.2  |-  ( ps 
->  ph )
Assertion
Ref Expression
impbii  |-  ( ph  <->  ps )

Proof of Theorem impbii
StepHypRef Expression
1 impbii.1 . 2  |-  ( ph  ->  ps )
2 impbii.2 . 2  |-  ( ps 
->  ph )
3 bi3 180 . 2  |-  ( (
ph  ->  ps )  -> 
( ( ps  ->  ph )  ->  ( ph  <->  ps ) ) )
41, 2, 3mp2 9 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  dfbi1  185  bicom  192  biid  228  2th  231  pm5.74  236  bitri  241  notnot  283  con34b  284  notbi  287  bibi2i  305  con1b  324  con2b  325  bi2.04  351  pm5.4  352  imdi  353  pm4.8  355  pm4.81  356  orcom  377  dfor2  401  impexp  434  ancom  438  oridm  501  orbi2i  506  or12  510  pm4.45im  546  pm4.44  561  pm4.79  567  anass  631  jaob  759  jcab  834  andi  838  pm4.72  847  oibabs  852  pm4.82  895  consensus  926  rnlem  932  3jaob  1246  truan  1340  dfnot  1341  3impexp  1375  3impexpbicom  1376  cad1  1407  tbw-bijust  1472  tbw-negdf  1473  19.26  1603  sbbii  1665  19.9v  1676  equcom  1692  19.3vOLD  1709  cbvalw  1714  cbvalvwOLD  1716  alcom  1752  19.3  1791  19.9hOLD  1795  19.23hOLD  1839  equsalhwOLD  1861  19.21hOLD  1862  excomOLD  1882  19.41  1900  19.41OLD  1901  cbval  1982  equsalOLD  2000  equsex  2002  ax12olem1  2005  ax12olem1OLD  2011  ax12olem3OLD  2013  equvin  2083  equs45f  2084  dfsb2  2115  sbnOLD  2118  sbim  2121  sbie  2122  sb6f  2127  sb5rf  2165  sb6rf  2166  sb9  2170  mo  2302  eu2  2305  mo2  2309  exmoeu  2322  euan  2337  2mo  2358  2eu6  2365  axext4  2419  cleqh  2532  nebi  2669  r19.26  2830  ralcom3  2865  ceqsex  2982  gencbvex  2990  gencbvex2  2991  eqvinc  3055  pm13.183  3068  rr19.3v  3069  rr19.28v  3070  euxfr2  3111  reu6  3115  reu3  3116  sbnfc2  3301  sspss  3438  unineq  3583  uneqin  3584  undif3  3594  difrab  3607  un00  3655  ssdifeq0  3702  r19.2zb  3710  ralf0  3726  elpr2  3825  snidb  3832  tppreqb  3931  difsnb  3932  pwpw0  3938  sssn  3949  preq12b  3966  preqsn  3972  pwsnALT  4002  unissint  4066  uniintsn  4079  iununi  4167  intex  4348  intnex  4349  iin0  4365  axpweq  4368  nfcvb  4386  sspwb  4405  unipw  4406  opnz  4424  opth  4427  opthwiener  4450  ssopab2b  4473  pwssun  4481  elon2  4584  unexb  4701  eusvnfb  4711  eusv2nf  4713  ralxfrALT  4734  uniexb  4744  iunpw  4751  ordeleqon  4761  onintrab  4773  unon  4803  onuninsuci  4812  ordzsl  4817  onzsl  4818  opelxp  4900  opthprc  4917  relop  5015  issetid  5019  xpid11  5083  elres  5173  iss  5181  issref  5239  asymref2  5243  xpnz  5284  ssrnres  5301  dfrel2  5313  relrelss  5385  unixp0  5395  fn0  5556  funssxp  5596  f00  5620  dffo2  5649  ffoss  5699  f1o00  5702  fo00  5703  fv3  5736  dffn5  5764  dff2  5873  dff3  5874  dffo4  5877  dffo5  5878  exfo  5879  fmpt  5882  ffnfv  5886  fsn  5898  fsn2  5900  fconstfv  5946  isores1  6046  ssoprab2b  6123  eqfnov2  6169  1st2ndb  6379  reldmtpos  6479  riotaundb  6583  abianfp  6708  omopthi  6892  mapsn  7047  mapsncnv  7052  mptelixpg  7091  elixpsn  7093  ixpsnf1o  7094  bren2  7130  en0  7162  en1  7166  en1b  7167  sbthb  7220  canth2  7252  onfin2  7290  sdom1  7300  1sdom  7303  fineqv  7316  unfilem1  7363  fiint  7375  pwfi  7394  unifpw  7401  wofib  7506  sucprcreg  7559  opthreg  7565  suc11reg  7566  infeq5  7584  rankwflemb  7711  r1elss  7724  pwwf  7725  unwf  7728  uniwf  7737  rankonid  7747  rankr1id  7780  rankuni  7781  rankxplim3  7797  scott0  7802  karden  7811  isnum3  7833  oncard  7839  card1  7847  cardlim  7851  cardmin2  7877  pm54.43lem  7878  ween  7908  acnnum  7925  alephsuc2  7953  alephgeom  7955  iscard3  7966  dfac3  7994  dfac4  7995  dfac5lem3  7998  dfac5  8001  dfac2  8003  dfac8  8007  dfac9  8008  dfacacn  8013  dfac13  8014  dfac12r  8018  dfac12k  8019  kmlem2  8023  kmlem13  8034  cdainf  8064  ackbij2  8115  cflim2  8135  isfin4-2  8186  isfin4-3  8187  isf33lem  8238  compsscnv  8243  fin1a2lem6  8277  domtriom  8315  ac9  8355  ac9s  8365  fodomb  8396  brdom3  8398  brdom5  8399  brdom4  8400  brdom7disj  8401  brdom6disj  8402  iunfo  8406  sdomsdomcard  8427  gch2  8546  gch3  8547  eltsk2g  8618  grutsk  8689  grothpw  8693  ordpipq  8811  ltbtwnnq  8847  mappsrpr  8975  map2psrpr  8977  elreal2  8999  le2tri3i  9195  ltadd2i  9196  elnn0nn  10254  elnnnn0b  10256  elnnnn0c  10257  elnnz  10284  elnn0z  10286  elz2  10290  elnnz1  10299  eluz2b2  10540  elnn1uz2  10544  elioo4g  10963  eluzfz2b  11058  fzn0  11062  elfz1end  11073  fzass4  11082  nn0fz0  11106  fzolb  11137  fzon0  11148  elfzo0  11163  elfzo1  11165  om2uzrani  11284  nn0opthi  11555  hashkf  11612  hashprb  11660  hashf1  11698  wrdexb  11755  sqr0lem  12038  rexanuz  12141  rexuz3  12144  fsum0diag  12553  sadcp1  12959  isprm6  13101  4sqlem4  13312  mreunirn  13818  isdrs2  14388  isacs5  14590  isacs4  14591  isacs3  14592  isnsg3  14966  gicer  15055  oppgmndb  15143  oppggrpb  15146  invghm  15445  opprrngb  15729  abvn0b  16354  gzrngunit  16756  zrngunit  16757  dvdsrz  16759  zlmlmod  16796  zlmassa  16797  cygth  16844  frgpcyg  16846  tgclb  17027  iscldtop  17151  isnrm2  17414  isnrm3  17415  discmp  17453  dfcon2  17474  2ndcsb  17504  dis2ndc  17515  loclly  17542  iskgen2  17572  dfac14  17642  kqtop  17769  kqt0  17770  kqreg  17775  kqnrm  17776  hmpher  17808  hmphsymb  17810  hmph0  17819  kqhmph  17843  ist1-5lem  17844  elmptrab2  17852  isfil2  17880  filunirn  17906  isufil2  17932  hausflim  18005  isfcls  18033  alexsubALT  18074  istgp2  18113  ustbas  18249  xmetunirn  18359  dscmet  18612  dscopn  18613  isngp4  18650  zcld  18836  zlmclm  19112  iscmet2  19239  iundisj  19434  i1f1lem  19573  fta1b  20084  elply2  20107  elqaa  20231  aannenlem2  20238  wilth  20846  lgsne0  21109  2sqlem2  21140  ostth  21325  uhgra0v  21337  wrdumgra  21343  usgra0v  21383  uvtx01vtx  21493  istrl2  21530  isspthonpth  21576  nmlno0lem  22286  isblo3i  22294  blocni  22298  hvsubeq0i  22557  hvaddcani  22559  bcseqi  22614  isch3  22736  norm1exi  22744  hhsssh  22761  shslubi  22879  dfch2  22901  pjoc1i  22925  pjchi  22926  shs00i  22944  chsscon3i  22955  chlejb1i  22970  chj00i  22981  shjshseli  22987  h1de2ctlem  23049  spanunsni  23073  cmcmi  23086  cmbr3i  23094  cmbr4i  23095  pj11i  23205  hosubeq0i  23321  dmadjrnb  23401  nmlnop0iALT  23490  lnopeq0i  23502  elunop2  23508  lnconi  23528  lncnopbd  23532  adjbdlnb  23579  adjbd1o  23580  adjeq0  23586  rnbra  23602  pjss1coi  23658  pjss2coi  23659  pjnormssi  23663  pjssdif2i  23669  pjssdif1i  23670  dfpjop  23677  pjinvari  23686  pjin2i  23688  pjci  23695  pjcmul1i  23696  pjcmul2i  23697  strb  23753  hstrbi  23761  mdsl1i  23816  atom1d  23848  chrelat2i  23860  cvbr4i  23862  cvexchi  23864  sumdmdi  23915  dmdbr4ati  23916  dmdbr5ati  23917  dmdbr6ati  23918  dmdbr7ati  23919  cdj3i  23936  difeq  23990  iundisjf  24021  iundisjfi  24144  xrge0tsmsbi  24216  issgon  24498  measbasedom  24548  ballotlem2  24738  ballotlemrinv  24783  nepss  25167  fprod0diag  25302  dfpo2  25370  dfon2  25411  distel  25423  elno2  25601  bdayfo  25622  fnimage  25766  altopthsn  25798  mptelee  25826  ellines  26078  rankeq1o  26104  df3nandALT1  26138  wl-pm5.74lem  26219  wl-nfnbi  26225  wl-exeq  26226  wl-aleq  26227  volsupnfl  26241  opnrebl2  26315  locfindis  26376  cover2  26406  isbnd3  26484  cntotbnd  26496  heibor  26521  isfld2  26606  isfldidl  26669  prtlem16  26709  funsnfsup  26734  ismrc  26746  isnacs3  26755  rexzrexnn0  26855  eldioph4b  26863  dford3  27090  wopprc  27092  ttac  27098  pw2f1ocnv  27099  dfac11  27128  dfac21  27132  isnumbasabl  27239  isnumbasgrp  27240  dfacbasgrp  27241  aaitgo  27335  pmtrfb  27374  pm10.55  27532  pm11.57  27556  sbeqalbi  27568  pm13.192  27578  pm13.194  27580  ipo0  27619  ifr0  27620  xpexb  27625  reuan  27925  afvfv0bi  27983  ffnafv  28002  fzo1fzo0n0  28111  usg2spthonot1  28310  frgra0v  28320  com3rgbi  28534  pm2.43bgbi  28537  pm2.43cbi  28538  sb5ALT  28546  trsbc  28562  2pm13.193  28576  a9e2ndeq  28583  2uasbanh  28585  eelT01  28755  eel0T1  28756  uunT1  28829  zfregs2VD  28890  equncomVD  28917  trsbcVD  28926  undif3VD  28931  2pm13.193VD  28952  a9e2eqVD  28956  a9e2ndeqVD  28958  2uasbanhVD  28960  a9e2ndeqALT  28980  bnj1533  29160  bnj983  29259  alcomwAUX7  29381  ax12olem3aAUX7  29394  equsalNEW7  29424  cbvalwwAUX7  29456  equvinNEW7  29466  sbnNEW7  29499  sbimNEW7  29502  sb5rfNEW7  29528  sb6rfNEW7  29529  sb8wAUX7  29530  equs45fNEW7  29558  sb6fNEW7  29570  dfsb2NEW7  29575  alcomw9bAUX7  29598  alcomOLD7  29618  excomOLD7  29631  cbvalOLD7  29662  nfsb4tw2AUXOLD7  29683  sbcomOLD7  29692  sb8OLD7  29693  sb9iOLD7  29695  sb9OLD7  29696  isltrn2N  30854
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