MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  impbii 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 19 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> 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  563  pm4.79  569  anass  633  jaob  761  jcab  836  andi  842  pm4.72  851  oibabs  856  pm4.82  899  consensus  930  rnlem  936  3jaob  1249  dfnot  1328  3impexp  1362  3impexpbicom  1363  cad1  1394  tbw-bijust  1458  tbw-negdf  1459  alcom  1568  19.26  1592  ax12o10lem13  1647  ax12o10lem14  1648  ax12olem16  1650  ax12olem17  1651  ax12olem21  1655  ax12olem23  1657  ax12olem27  1661  19.3  1760  excom  1765  19.41  1799  equcom  1824  equsal  1851  equsalh  1852  cbval  1877  sbbii  1886  equs45f  1915  sb6f  1916  dfsb2  1948  sbn  1955  sbim  1958  sb5rf  1985  sb6rf  1986  sb8  1987  sb9  1990  equvin  2000  mo  2140  eu2  2143  mo2  2147  exmoeu  2160  euan  2175  2mo  2196  2eu6  2203  axext4  2242  cleqh  2355  nebi  2492  r19.26  2650  ralcom3  2680  ceqsex  2797  gencbvex  2805  gencbvex2  2806  eqvinc  2870  pm13.183  2883  rr19.3v  2884  rr19.28v  2885  euxfr2  2925  reu6  2929  reu3  2930  sbnfc2  3116  sspss  3250  unineq  3394  uneqin  3395  undif3  3404  difrab  3417  un00  3465  ssdifeq0  3511  r19.2zb  3519  ralf0  3535  elpr2  3633  snidb  3640  difsneq  3731  pwpw0  3737  sssn  3746  preq12b  3762  preqsn  3766  pwsnALT  3796  unissint  3860  uniintsn  3873  iununi  3960  intex  4143  intnex  4144  iin0  4156  axpweq  4159  nfcvb  4177  sspwb  4195  unipw  4196  opnz  4214  opth  4217  opthwiener  4240  ssopab2b  4263  pwssun  4271  pwundifOLD  4273  elon2  4375  unexb  4492  eusvnfb  4502  eusv2nf  4504  ralxfrALT  4525  uniexb  4535  iunpw  4542  ordeleqon  4552  onintrab  4564  unon  4594  onuninsuci  4603  ordzsl  4608  onzsl  4609  opelxp  4707  opthprc  4724  relop  4822  issetid  4826  xpid11  4888  elres  4978  iss  4986  issref  5044  asymref2  5048  xpnz  5087  ssrnres  5104  dfrel2  5112  relrelss  5183  unixp0  5193  fn0  5301  funssxp  5340  f00  5364  dffo2  5393  ffoss  5443  f1o00  5446  fo00  5447  fv3  5474  dffn5  5502  dff2  5606  dff3  5607  dffo4  5610  dffo5  5611  exfo  5612  fmpt  5615  ffnfv  5619  fsn  5630  fsn2  5632  fconstfv  5668  isores1  5765  ssoprab2b  5839  eqfnov2  5885  1st2ndb  6094  reldmtpos  6176  riotaundb  6314  abianfp  6439  omopthi  6623  mapsn  6777  mapsncnv  6782  mptelixpg  6821  elixpsn  6823  ixpsnf1o  6824  bren2  6860  en0  6892  en1  6896  en1b  6897  sbthb  6950  canth2  6982  onfin2  7020  sdom1  7030  1sdom  7033  fineqv  7046  unfilem1  7089  fiint  7101  pwfi  7119  unifpw  7126  wofib  7228  sucprcreg  7281  opthreg  7287  suc11reg  7288  infeq5  7306  rankwflemb  7433  r1elss  7446  pwwf  7447  unwf  7450  uniwf  7459  rankonid  7469  rankr1id  7502  rankuni  7503  rankxplim3  7519  scott0  7524  karden  7533  isnum3  7555  oncard  7561  card1  7569  cardlim  7573  cardmin2  7599  pm54.43lem  7600  ween  7630  acnnum  7647  alephsuc2  7675  alephgeom  7677  iscard3  7688  dfac3  7716  dfac4  7717  dfac5lem3  7720  dfac5  7723  dfac2  7725  dfac8  7729  dfac9  7730  dfacacn  7735  dfac13  7736  dfac12r  7740  dfac12k  7741  kmlem2  7745  kmlem13  7756  cdainf  7786  ackbij2  7837  cflim2  7857  isfin4-2  7908  isfin4-3  7909  isf33lem  7960  compsscnv  7965  fin1a2lem6  7999  domtriom  8037  ac9  8078  ac9s  8088  fodomb  8119  brdom3  8121  brdom5  8122  brdom4  8123  brdom7disj  8124  brdom6disj  8125  iunfo  8129  sdomsdomcard  8150  gch2  8269  gch3  8270  eltsk2g  8341  grutsk  8412  grothpw  8416  ordpipq  8534  ltbtwnnq  8570  mappsrpr  8698  map2psrpr  8700  elreal2  8722  le2tri3i  8917  ltadd2i  8918  elnn0nn  9974  elnnnn0b  9976  elnnnn0c  9977  elnnz  10002  elnn0z  10004  elz2  10008  elnnz1  10017  eluz2b2  10258  elnn1uz2  10262  elioo4g  10678  eluzfz2b  10772  fzn0  10776  elfz1end  10787  fzass4  10796  fzolb  10847  fzon0  10858  elfzo0  10871  om2uzrani  10982  nn0opthi  11252  hashkf  11306  hashf1  11361  wrdexb  11415  sqr0lem  11692  rexanuz  11795  rexuz3  11798  fsum0diag  12206  sadcp1  12609  isprm6  12751  4sqlem4  12962  mreunirn  13466  isdrs2  14036  isacs5  14238  isacs4  14239  isacs3  14240  isnsg3  14614  gicer  14703  oppgmndb  14791  oppggrpb  14794  invghm  15093  opprrngb  15377  abvn0b  16006  gzrngunit  16400  zrngunit  16401  dvdsrz  16403  zlmlmod  16440  zlmassa  16441  cygth  16488  frgpcyg  16490  tgclb  16671  iscldtop  16795  isnrm2  17049  isnrm3  17050  discmp  17088  dfcon2  17108  2ndcsb  17138  dis2ndc  17149  loclly  17176  iskgen2  17206  dfac14  17275  kqtop  17399  kqt0  17400  kqreg  17405  kqnrm  17406  hmpher  17438  hmphsymb  17440  hmph0  17449  kqhmph  17473  ist1-5lem  17474  elmptrab2  17486  isfil2  17514  filunirn  17540  isufil2  17566  hausflim  17639  isfcls  17667  alexsubALT  17708  istgp2  17737  xmetunirn  17865  dscmet  18058  dscopn  18059  isngp4  18096  zcld  18282  zlmclm  18556  iscmet2  18683  iundisj  18868  i1f1lem  19007  fta1b  19518  elply2  19541  elqaa  19665  aannenlem2  19672  wilth  20272  lgsne0  20535  2sqlem2  20566  ostth  20751  nmlno0lem  21332  isblo3i  21340  blocni  21344  hvsubeq0i  21603  hvaddcani  21605  bcseqi  21660  isch3  21782  norm1exi  21790  hhsssh  21807  shslubi  21925  dfch2  21947  pjoc1i  21971  pjchi  21972  shs00i  21990  chsscon3i  22001  chlejb1i  22016  chj00i  22027  shjshseli  22033  h1de2ctlem  22095  spanunsni  22119  cmcmi  22132  cmbr3i  22140  cmbr4i  22141  pj11i  22251  hosubeq0i  22367  dmadjrnb  22447  nmlnop0iALT  22536  lnopeq0i  22548  elunop2  22554  lnconi  22574  lncnopbd  22578  adjbdlnb  22625  adjbd1o  22626  adjeq0  22632  rnbra  22648  pjss1coi  22704  pjss2coi  22705  pjnormssi  22709  pjssdif2i  22715  pjssdif1i  22716  dfpjop  22723  pjinvari  22732  pjin2i  22734  pjci  22741  pjcmul1i  22742  pjcmul2i  22743  strb  22799  hstrbi  22807  mdsl1i  22862  atom1d  22894  chrelat2i  22906  cvbr4i  22908  cvexchi  22910  sumdmdi  22961  dmdbr4ati  22962  dmdbr5ati  22963  dmdbr6ati  22964  dmdbr7ati  22965  cdj3i  22982  ballotlem2  23009  ballotlemrinv  23054  wrdumgra  23241  nepss  23445  dfpo2  23484  dfon2  23518  distel  23530  elno2  23677  axbday  23698  elfix  23820  dffix2  23822  fnimage  23844  altopthsn  23871  mptelee  23899  ellines  24151  rankeq1o  24177  df3nandALT1  24211  wl-pm5.74lem  24293  and4as  24306  altdftru  24315  trcrm  24318  facrm  24320  bibox  24349  binxt  24351  nxtor  24352  nxtand  24353  bidia  24356  evpexun  24365  alalifal  24370  boxand  24373  axlll2  24395  dmoprabss6  24402  restidsing  24443  fixpc  24461  sssu  24509  dstr  24539  definc  24647  domncnt  24650  ranncnt  24651  dfps2  24657  sallnei  24897  altretop  24968  addcanri  25034  bisig0  25430  opnrebl2  25604  locfindis  25673  cover2  25726  isbnd3  25876  cntotbnd  25888  heibor  25913  isfld2  25998  isfldidl  26061  prtlem16  26105  funsnfsup  26130  ismrc  26144  isnacs3  26153  rexzrexnn0  26253  eldioph4b  26262  dford3  26489  wopprc  26491  ttac  26497  pw2f1ocnv  26498  dfac11  26528  dfac21  26532  isnumbasabl  26639  isnumbasgrp  26640  dfacbasgrp  26641  aaitgo  26735  pmtrfb  26774  pm10.55  26932  pm11.57  26956  sbeqalbi  26968  pm13.192  26979  pm13.194  26981  ipo0  27021  ifr0  27022  xpexb  27027  reuan  27307  com3rgbi  27412  pm2.43bgbi  27415  pm2.43cbi  27416  sb5ALT  27424  trsbc  27440  2pm13.193  27454  a9e2ndeq  27461  2uasbanh  27463  eelT01  27622  eel0T1  27623  uunT1  27688  zfregs2VD  27750  equncomVD  27777  trsbcVD  27786  undif3VD  27791  2pm13.193VD  27812  a9e2eqVD  27816  a9e2ndeqVD  27818  2uasbanhVD  27820  a9e2ndeqALT  27841  bnj1533  28016  bnj983  28115  albiiK  28242  19.8vK  28254  cbvalK  28261  cbvalvK  28262  ax12o10lem13K  28304  ax12o10lem13X  28305  ax12o10lem14K  28306  ax12o10lem14X  28307  equvinvK  28310  ax12olem16K  28311  ax12olem16X  28312  ax12olem17K  28313  ax12olem17X  28314  ax12olem21K  28321  ax12olem21X  28322  equextvK  28323  ax12olem23X  28327  ax12olem27X  28332  equvinv  28364  equvelv  28366  isltrn2N  29559
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator