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  1850  equsalh  1851  cbval  1876  sbbii  1885  equs45f  1914  sb6f  1915  dfsb2  1947  sbn  1954  sbim  1957  sb5rf  1984  sb6rf  1985  sb8  1986  sb9  1989  equvin  1999  mo  2135  eu2  2138  mo2  2142  exmoeu  2155  euan  2170  2mo  2191  2eu6  2198  axext4  2237  cleqh  2346  nebi  2483  r19.26  2637  ralcom3  2667  ceqsex  2760  gencbvex  2768  gencbvex2  2769  eqvinc  2832  pm13.183  2845  rr19.3v  2846  rr19.28v  2847  euxfr2  2887  reu6  2893  reu3  2894  sbnfc2  3069  sspss  3195  unineq  3326  uneqin  3327  undif3  3336  difrab  3349  un00  3397  ssdifeq0  3442  r19.2zb  3450  ralf0  3466  elpr2  3563  snidb  3570  pwpw0  3663  sssn  3672  preq12b  3688  preqsn  3692  pwsnALT  3722  unissint  3784  uniintsn  3797  iununi  3884  intex  4065  intnex  4066  iin0  4078  axpweq  4081  nfcvb  4099  sspwb  4117  unipw  4118  opnz  4135  opth  4138  opthwiener  4161  ssopab2b  4184  pwssun  4192  pwundifOLD  4194  elon2  4296  unexb  4411  eusvnfb  4421  eusv2nf  4423  ralxfrALT  4444  uniexb  4454  iunpw  4461  ordeleqon  4471  onintrab  4483  unon  4513  onuninsuci  4522  ordzsl  4527  onzsl  4528  opelxp  4626  opthprc  4643  relop  4741  issetid  4745  xpid11  4807  elres  4897  iss  4905  issref  4963  asymref2  4967  xpnz  5006  ssrnres  5023  dfrel2  5031  relrelss  5102  unixp0  5112  fn0  5220  funssxp  5259  f00  5283  dffo2  5312  ffoss  5362  f1o00  5365  fo00  5366  fv3  5393  dffn5  5420  dff2  5524  dff3  5525  dffo4  5528  dffo5  5529  exfo  5530  fmpt  5533  ffnfv  5537  fsn  5548  fsn2  5550  fconstfv  5586  isores1  5683  ssoprab2b  5757  eqfnov2  5803  1st2ndb  6012  reldmtpos  6094  riotaundb  6232  abianfp  6357  omopthi  6541  mapsn  6695  mapsncnv  6700  mptelixpg  6739  elixpsn  6741  ixpsnf1o  6742  bren2  6778  en0  6809  en1  6813  en1b  6814  sbthb  6867  canth2  6899  onfin2  6937  sdom1  6947  1sdom  6950  fineqv  6963  unfilem1  7006  fiint  7018  pwfi  7035  unifpw  7042  wofib  7144  sucprcreg  7197  opthreg  7203  suc11reg  7204  infeq5  7222  rankwflemb  7349  r1elss  7362  pwwf  7363  unwf  7366  uniwf  7375  rankonid  7385  rankr1id  7418  rankuni  7419  rankxplim3  7435  scott0  7440  karden  7449  isnum3  7471  oncard  7477  card1  7485  cardlim  7489  cardmin2  7515  pm54.43lem  7516  ween  7546  acnnum  7563  alephsuc2  7591  alephgeom  7593  iscard3  7604  dfac3  7632  dfac4  7633  dfac5lem3  7636  dfac5  7639  dfac2  7641  dfac8  7645  dfac9  7646  dfacacn  7651  dfac13  7652  dfac12r  7656  dfac12k  7657  kmlem2  7661  kmlem13  7672  cdainf  7702  ackbij2  7753  cflim2  7773  isfin4-2  7824  isfin4-3  7825  isf33lem  7876  compsscnv  7881  fin1a2lem6  7915  domtriom  7953  ac9  7994  ac9s  8004  fodomb  8035  brdom3  8037  brdom5  8038  brdom4  8039  brdom7disj  8040  brdom6disj  8041  iunfo  8045  sdomsdomcard  8064  gch2  8181  gch3  8182  eltsk2g  8253  grutsk  8324  grothpw  8328  ordpipq  8446  ltbtwnnq  8482  mappsrpr  8610  map2psrpr  8612  elreal2  8634  le2tri3i  8829  ltadd2i  8830  elnn0nn  9885  elnnnn0b  9887  elnnnn0c  9888  elnnz  9913  elnn0z  9915  elz2  9919  elnnz1  9928  eluz2b2  10169  elnn1uz2  10173  elioo4g  10589  eluzfz2b  10683  fzn0  10687  elfz1end  10698  fzass4  10707  fzolb  10758  fzon0  10769  elfzo0  10782  om2uzrani  10893  nn0opthi  11163  hashkf  11217  hashf1  11272  wrdexb  11326  sqr0lem  11603  rexanuz  11706  rexuz3  11709  fsum0diag  12117  sadcp1  12520  isprm6  12662  4sqlem4  12873  mreunirn  13375  isdrs2  13917  isacs5  14119  isacs4  14120  isacs3  14121  isnsg3  14486  gicer  14575  oppgmndb  14663  oppggrpb  14666  invghm  14965  opprrngb  15249  abvn0b  15875  gzrngunit  16269  zrngunit  16270  dvdsrz  16272  zlmlmod  16309  zlmassa  16310  cygth  16357  frgpcyg  16359  tgclb  16540  iscldtop  16664  isnrm2  16918  isnrm3  16919  discmp  16957  dfcon2  16977  2ndcsb  17007  dis2ndc  17018  loclly  17045  iskgen2  17075  dfac14  17144  kqtop  17268  kqt0  17269  kqreg  17274  kqnrm  17275  hmpher  17307  hmphsymb  17309  hmph0  17318  kqhmph  17342  ist1-5lem  17343  elmptrab2  17355  isfil2  17383  filunirn  17409  isufil2  17435  hausflim  17508  isfcls  17536  alexsubALT  17577  istgp2  17606  xmetunirn  17734  dscmet  17927  dscopn  17928  isngp4  17965  zcld  18151  zlmclm  18425  iscmet2  18552  iundisj  18737  i1f1lem  18876  fta1b  19387  elply2  19410  elqaa  19534  aannenlem2  19541  wilth  20141  lgsne0  20404  2sqlem2  20435  ostth  20620  nmlno0lem  21201  isblo3i  21209  blocni  21213  hvsubeq0i  21472  hvaddcani  21474  bcseqi  21529  isch3  21651  norm1exi  21659  hhsssh  21676  shslubi  21794  dfch2  21816  pjoc1i  21840  pjchi  21841  shs00i  21859  chsscon3i  21870  chlejb1i  21885  chj00i  21896  shjshseli  21902  h1de2ctlem  21964  spanunsni  21988  cmcmi  22019  cmbr3i  22027  cmbr4i  22028  pj11i  22138  hosubeq0i  22236  dmadjrnb  22316  nmlnop0iALT  22405  lnopeq0i  22417  elunop2  22423  lnconi  22443  lncnopbd  22447  adjbdlnb  22494  adjbd1o  22495  adjeq0  22501  rnbra  22517  pjss1coi  22573  pjss2coi  22574  pjnormssi  22578  pjssdif2i  22584  pjssdif1i  22585  dfpjop  22592  pjinvari  22601  pjin2i  22603  pjci  22610  pjcmul1i  22611  pjcmul2i  22612  strb  22668  hstrbi  22676  mdsl1i  22731  atom1d  22763  chrelat2i  22775  cvbr4i  22777  cvexchi  22779  sumdmdi  22830  dmdbr4ati  22831  dmdbr5ati  22832  dmdbr6ati  22833  dmdbr7ati  22834  cdj3i  22851  wrdumgra  23039  nepss  23243  dfpo2  23282  dfon2  23316  distel  23328  elno2  23475  axbday  23496  elfix  23618  dffix2  23620  fnimage  23642  altopthsn  23669  mptelee  23697  ellines  23949  rankeq1o  23975  df3nandALT1  24009  wl-pm5.74lem  24091  and4as  24104  altdftru  24113  trcrm  24116  facrm  24118  bibox  24147  binxt  24149  nxtor  24150  nxtand  24151  bidia  24154  evpexun  24163  alalifal  24168  boxand  24171  axlll2  24193  dmoprabss6  24200  restidsing  24241  fixpc  24259  sssu  24307  dstr  24337  definc  24445  domncnt  24448  ranncnt  24449  dfps2  24455  sallnei  24695  altretop  24766  addcanri  24832  bisig0  25228  opnrebl2  25402  locfindis  25471  cover2  25524  isbnd3  25674  cntotbnd  25686  heibor  25711  isfld2  25796  isfldidl  25859  prtlem16  25903  funsnfsup  25928  ismrc  25942  isnacs3  25951  rexzrexnn0  26051  eldioph4b  26060  dford3  26287  wopprc  26289  ttac  26295  pw2f1ocnv  26296  dfac11  26326  dfac21  26330  isnumbasabl  26437  isnumbasgrp  26438  dfacbasgrp  26439  aaitgo  26533  pmtrfb  26572  pm10.55  26730  pm11.57  26754  sbeqalbi  26766  pm13.192  26777  pm13.194  26779  ipo0  26819  ifr0  26820  xpexb  26825  com3rgbi  26969  pm2.43bgbi  26972  pm2.43cbi  26973  sb5ALT  26981  trsbc  26997  2pm13.193  27011  a9e2ndeq  27018  2uasbanh  27020  eelT01  27179  eel0T1  27180  uunT1  27245  zfregs2VD  27307  equncomVD  27334  trsbcVD  27343  undif3VD  27348  2pm13.193VD  27369  a9e2eqVD  27373  a9e2ndeqVD  27375  2uasbanhVD  27377  a9e2ndeqALT  27398  bnj1533  27573  bnj983  27672  equvinv  27803  equvelv  27805  isltrn2N  28998
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