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

Theorem impbii 182
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 181 . 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 178
This theorem is referenced by:  dfbi1  186  bicom  193  biid  229  2th  232  pm5.74  237  bitri  242  notnot  284  con34b  285  notbi  288  bibi2i  306  con1b  325  con2b  326  bi2.04  352  pm5.4  353  imdi  354  pm4.8  356  pm4.81  357  orcom  378  dfor2  402  impexp  435  ancom  439  oridm  502  orbi2i  507  or12  511  pm4.45im  547  pm4.44  562  pm4.79  568  anass  632  jaob  760  jcab  835  andi  839  pm4.72  848  oibabs  853  pm4.82  896  consensus  927  rnlem  933  3jaob  1247  truan  1341  dfnot  1342  3impexp  1376  3impexpbicom  1377  cad1  1408  tbw-bijust  1473  tbw-negdf  1474  19.26  1604  sbbii  1666  19.9v  1677  equcom  1693  19.3vOLD  1710  cbvalw  1715  cbvalvwOLD  1717  alcom  1753  19.3  1792  19.9hOLD  1796  19.23hOLD  1840  equsalhwOLD  1862  19.21hOLD  1863  excomOLD  1883  19.41  1901  19.41OLD  1902  cbval  1983  equsalOLD  2001  equsex  2003  ax12olem1  2006  ax12olem1OLD  2012  ax12olem3OLD  2014  equvin  2088  equs45f  2089  dfsb2  2110  sb6f  2124  sbnOLD  2133  sbim  2137  sb5rf  2168  sb6rf  2169  sb9  2173  mo  2305  eu2  2308  mo2  2312  exmoeu  2325  euan  2340  2mo  2361  2eu6  2368  axext4  2422  cleqh  2535  nebi  2677  r19.26  2840  ralcom3  2875  ceqsex  2992  gencbvex  3000  gencbvex2  3001  eqvinc  3065  pm13.183  3078  rr19.3v  3079  rr19.28v  3080  euxfr2  3121  reu6  3125  reu3  3126  sbnfc2  3311  sspss  3448  unineq  3593  uneqin  3594  undif3  3604  difrab  3617  un00  3665  ssdifeq0  3712  r19.2zb  3720  ralf0  3736  elpr2  3835  snidb  3842  tppreqb  3941  difsnb  3942  pwpw0  3948  sssn  3959  preq12b  3976  preqsn  3982  pwsnALT  4012  unissint  4076  uniintsn  4089  iununi  4178  intex  4359  intnex  4360  iin0  4376  axpweq  4379  nfcvb  4397  sspwb  4416  unipw  4417  opnz  4435  opth  4438  opthwiener  4461  ssopab2b  4484  pwssun  4492  elon2  4595  unexb  4712  eusvnfb  4722  eusv2nf  4724  ralxfrALT  4745  uniexb  4755  iunpw  4762  ordeleqon  4772  onintrab  4784  unon  4814  onuninsuci  4823  ordzsl  4828  onzsl  4829  opelxp  4911  opthprc  4928  relop  5026  issetid  5030  xpid11  5094  elres  5184  iss  5192  issref  5250  asymref2  5254  xpnz  5295  ssrnres  5312  dfrel2  5324  relrelss  5396  unixp0  5406  fn0  5567  funssxp  5607  f00  5631  dffo2  5660  ffoss  5710  f1o00  5713  fo00  5714  fv3  5747  dffn5  5775  dff2  5884  dff3  5885  dffo4  5888  dffo5  5889  exfo  5890  fmpt  5893  ffnfv  5897  fsn  5909  fsn2  5911  fconstfv  5957  isores1  6057  ssoprab2b  6134  eqfnov2  6180  1st2ndb  6390  reldmtpos  6490  riotaundb  6594  abianfp  6719  omopthi  6903  mapsn  7058  mapsncnv  7063  mptelixpg  7102  elixpsn  7104  ixpsnf1o  7105  bren2  7141  en0  7173  en1  7177  en1b  7178  sbthb  7231  canth2  7263  onfin2  7301  sdom1  7311  1sdom  7314  fineqv  7327  unfilem1  7374  fiint  7386  pwfi  7405  unifpw  7412  wofib  7517  sucprcreg  7570  opthreg  7576  suc11reg  7577  infeq5  7595  rankwflemb  7722  r1elss  7735  pwwf  7736  unwf  7739  uniwf  7748  rankonid  7758  rankr1id  7791  rankuni  7792  rankxplim3  7810  scott0  7815  karden  7824  isnum3  7846  oncard  7852  card1  7860  cardlim  7864  cardmin2  7890  pm54.43lem  7891  ween  7921  acnnum  7938  alephsuc2  7966  alephgeom  7968  iscard3  7979  dfac3  8007  dfac4  8008  dfac5lem3  8011  dfac5  8014  dfac2  8016  dfac8  8020  dfac9  8021  dfacacn  8026  dfac13  8027  dfac12r  8031  dfac12k  8032  kmlem2  8036  kmlem13  8047  cdainf  8077  ackbij2  8128  cflim2  8148  isfin4-2  8199  isfin4-3  8200  isf33lem  8251  compsscnv  8256  fin1a2lem6  8290  domtriom  8328  ac9  8368  ac9s  8378  fodomb  8409  brdom3  8411  brdom5  8412  brdom4  8413  brdom7disj  8414  brdom6disj  8415  iunfo  8419  sdomsdomcard  8440  gch2  8555  gch3  8556  eltsk2g  8631  grutsk  8702  grothpw  8706  ordpipq  8824  ltbtwnnq  8860  mappsrpr  8988  map2psrpr  8990  elreal2  9012  le2tri3i  9208  ltadd2i  9209  elnn0nn  10267  elnnnn0b  10269  elnnnn0c  10270  elnnz  10297  elnn0z  10299  elz2  10303  elnnz1  10312  eluz2b2  10553  elnn1uz2  10557  elioo4g  10976  eluzfz2b  11071  fzn0  11075  elfz1end  11086  fzass4  11095  nn0fz0  11119  fzolb  11150  fzon0  11161  elfzo0  11176  elfzo1  11178  om2uzrani  11297  nn0opthi  11568  hashkf  11625  hashprb  11673  hashf1  11711  wrdexb  11768  sqr0lem  12051  rexanuz  12154  rexuz3  12157  fsum0diag  12566  sadcp1  12972  isprm6  13114  4sqlem4  13325  mreunirn  13831  isdrs2  14401  isacs5  14603  isacs4  14604  isacs3  14605  isnsg3  14979  gicer  15068  oppgmndb  15156  oppggrpb  15159  invghm  15458  opprrngb  15742  abvn0b  16367  gzrngunit  16769  zrngunit  16770  dvdsrz  16772  zlmlmod  16809  zlmassa  16810  cygth  16857  frgpcyg  16859  tgclb  17040  iscldtop  17164  isnrm2  17427  isnrm3  17428  discmp  17466  dfcon2  17487  2ndcsb  17517  dis2ndc  17528  loclly  17555  iskgen2  17585  dfac14  17655  kqtop  17782  kqt0  17783  kqreg  17788  kqnrm  17789  hmpher  17821  hmphsymb  17823  hmph0  17832  kqhmph  17856  ist1-5lem  17857  elmptrab2  17865  isfil2  17893  filunirn  17919  isufil2  17945  hausflim  18018  isfcls  18046  alexsubALT  18087  istgp2  18126  ustbas  18262  xmetunirn  18372  dscmet  18625  dscopn  18626  isngp4  18663  zcld  18849  zlmclm  19125  iscmet2  19252  iundisj  19447  i1f1lem  19584  fta1b  20097  elply2  20120  elqaa  20244  aannenlem2  20251  wilth  20859  lgsne0  21122  2sqlem2  21153  ostth  21338  uhgra0v  21350  wrdumgra  21356  usgra0v  21396  uvtx01vtx  21506  istrl2  21543  isspthonpth  21589  nmlno0lem  22299  isblo3i  22307  blocni  22311  hvsubeq0i  22570  hvaddcani  22572  bcseqi  22627  isch3  22749  norm1exi  22757  hhsssh  22774  shslubi  22892  dfch2  22914  pjoc1i  22938  pjchi  22939  shs00i  22957  chsscon3i  22968  chlejb1i  22983  chj00i  22994  shjshseli  23000  h1de2ctlem  23062  spanunsni  23086  cmcmi  23099  cmbr3i  23107  cmbr4i  23108  pj11i  23218  hosubeq0i  23334  dmadjrnb  23414  nmlnop0iALT  23503  lnopeq0i  23515  elunop2  23521  lnconi  23541  lncnopbd  23545  adjbdlnb  23592  adjbd1o  23593  adjeq0  23599  rnbra  23615  pjss1coi  23671  pjss2coi  23672  pjnormssi  23676  pjssdif2i  23682  pjssdif1i  23683  dfpjop  23690  pjinvari  23699  pjin2i  23701  pjci  23708  pjcmul1i  23709  pjcmul2i  23710  strb  23766  hstrbi  23774  mdsl1i  23829  atom1d  23861  chrelat2i  23873  cvbr4i  23875  cvexchi  23877  sumdmdi  23928  dmdbr4ati  23929  dmdbr5ati  23930  dmdbr6ati  23931  dmdbr7ati  23932  cdj3i  23949  difeq  24003  iundisjf  24034  iundisjfi  24157  xrge0tsmsbi  24229  issgon  24511  measbasedom  24561  ballotlem2  24751  ballotlemrinv  24796  nepss  25180  fprod0diag  25315  dfpo2  25383  dfon2  25424  distel  25436  elno2  25614  bdayfo  25635  fnimage  25779  altopthsn  25811  mptelee  25839  ellines  26091  rankeq1o  26117  df3nandALT1  26151  wl-pm5.74lem  26232  wl-nfnbi  26238  wl-exeq  26239  wl-aleq  26240  volsupnfl  26263  dvtanlem  26268  opnrebl2  26338  locfindis  26399  cover2  26429  isbnd3  26507  cntotbnd  26519  heibor  26544  isfld2  26629  isfldidl  26692  prtlem16  26732  funsnfsup  26757  ismrc  26769  isnacs3  26778  rexzrexnn0  26878  eldioph4b  26886  dford3  27113  wopprc  27115  ttac  27121  pw2f1ocnv  27122  dfac11  27151  dfac21  27155  isnumbasabl  27262  isnumbasgrp  27263  dfacbasgrp  27264  aaitgo  27358  pmtrfb  27397  pm10.55  27555  pm11.57  27579  sbeqalbi  27591  pm13.192  27601  pm13.194  27603  ipo0  27642  ifr0  27643  xpexb  27648  reuan  27948  afvfv0bi  28006  ffnafv  28025  f0bi  28092  fzo1fzo0n0  28151  usg2spthonot1  28422  frgra0v  28457  com3rgbi  28671  pm2.43bgbi  28674  pm2.43cbi  28675  sb5ALT  28683  trsbc  28699  2pm13.193  28713  a9e2ndeq  28720  2uasbanh  28722  eelT01  28892  eel0T1  28893  uunT1  28966  zfregs2VD  29027  equncomVD  29054  trsbcVD  29063  undif3VD  29068  2pm13.193VD  29089  a9e2eqVD  29093  a9e2ndeqVD  29095  2uasbanhVD  29097  a9e2ndeqALT  29117  bnj1533  29297  bnj983  29396  alcomwAUX7  29518  ax12olem3aAUX7  29531  equsalNEW7  29561  cbvalwwAUX7  29593  equvinNEW7  29603  sbnNEW7  29636  sbimNEW7  29639  sb5rfNEW7  29665  sb6rfNEW7  29666  sb8wAUX7  29667  equs45fNEW7  29695  sb6fNEW7  29707  dfsb2NEW7  29712  alcomw9bAUX7  29735  alcomOLD7  29755  excomOLD7  29768  cbvalOLD7  29799  nfsb4tw2AUXOLD7  29820  sbcomOLD7  29829  sb8OLD7  29830  sb9iOLD7  29832  sb9OLD7  29833  isltrn2N  30991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator