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  2138  eu2  2141  mo2  2145  exmoeu  2158  euan  2173  2mo  2194  2eu6  2201  axext4  2240  cleqh  2353  nebi  2490  r19.26  2646  ralcom3  2676  ceqsex  2773  gencbvex  2781  gencbvex2  2782  eqvinc  2846  pm13.183  2859  rr19.3v  2860  rr19.28v  2861  euxfr2  2901  reu6  2907  reu3  2908  sbnfc2  3083  sspss  3217  unineq  3361  uneqin  3362  undif3  3371  difrab  3384  un00  3432  ssdifeq0  3478  r19.2zb  3486  ralf0  3502  elpr2  3600  snidb  3607  difsneq  3698  pwpw0  3704  sssn  3713  preq12b  3729  preqsn  3733  pwsnALT  3763  unissint  3827  uniintsn  3840  iununi  3927  intex  4109  intnex  4110  iin0  4122  axpweq  4125  nfcvb  4143  sspwb  4161  unipw  4162  opnz  4179  opth  4182  opthwiener  4205  ssopab2b  4228  pwssun  4236  pwundifOLD  4238  elon2  4340  unexb  4457  eusvnfb  4467  eusv2nf  4469  ralxfrALT  4490  uniexb  4500  iunpw  4507  ordeleqon  4517  onintrab  4529  unon  4559  onuninsuci  4568  ordzsl  4573  onzsl  4574  opelxp  4672  opthprc  4689  relop  4787  issetid  4791  xpid11  4853  elres  4943  iss  4951  issref  5009  asymref2  5013  xpnz  5052  ssrnres  5069  dfrel2  5077  relrelss  5148  unixp0  5158  fn0  5266  funssxp  5305  f00  5329  dffo2  5358  ffoss  5408  f1o00  5411  fo00  5412  fv3  5439  dffn5  5467  dff2  5571  dff3  5572  dffo4  5575  dffo5  5576  exfo  5577  fmpt  5580  ffnfv  5584  fsn  5595  fsn2  5597  fconstfv  5633  isores1  5730  ssoprab2b  5804  eqfnov2  5850  1st2ndb  6059  reldmtpos  6141  riotaundb  6279  abianfp  6404  omopthi  6588  mapsn  6742  mapsncnv  6747  mptelixpg  6786  elixpsn  6788  ixpsnf1o  6789  bren2  6825  en0  6857  en1  6861  en1b  6862  sbthb  6915  canth2  6947  onfin2  6985  sdom1  6995  1sdom  6998  fineqv  7011  unfilem1  7054  fiint  7066  pwfi  7084  unifpw  7091  wofib  7193  sucprcreg  7246  opthreg  7252  suc11reg  7253  infeq5  7271  rankwflemb  7398  r1elss  7411  pwwf  7412  unwf  7415  uniwf  7424  rankonid  7434  rankr1id  7467  rankuni  7468  rankxplim3  7484  scott0  7489  karden  7498  isnum3  7520  oncard  7526  card1  7534  cardlim  7538  cardmin2  7564  pm54.43lem  7565  ween  7595  acnnum  7612  alephsuc2  7640  alephgeom  7642  iscard3  7653  dfac3  7681  dfac4  7682  dfac5lem3  7685  dfac5  7688  dfac2  7690  dfac8  7694  dfac9  7695  dfacacn  7700  dfac13  7701  dfac12r  7705  dfac12k  7706  kmlem2  7710  kmlem13  7721  cdainf  7751  ackbij2  7802  cflim2  7822  isfin4-2  7873  isfin4-3  7874  isf33lem  7925  compsscnv  7930  fin1a2lem6  7964  domtriom  8002  ac9  8043  ac9s  8053  fodomb  8084  brdom3  8086  brdom5  8087  brdom4  8088  brdom7disj  8089  brdom6disj  8090  iunfo  8094  sdomsdomcard  8115  gch2  8234  gch3  8235  eltsk2g  8306  grutsk  8377  grothpw  8381  ordpipq  8499  ltbtwnnq  8535  mappsrpr  8663  map2psrpr  8665  elreal2  8687  le2tri3i  8882  ltadd2i  8883  elnn0nn  9938  elnnnn0b  9940  elnnnn0c  9941  elnnz  9966  elnn0z  9968  elz2  9972  elnnz1  9981  eluz2b2  10222  elnn1uz2  10226  elioo4g  10642  eluzfz2b  10736  fzn0  10740  elfz1end  10751  fzass4  10760  fzolb  10811  fzon0  10822  elfzo0  10835  om2uzrani  10946  nn0opthi  11216  hashkf  11270  hashf1  11325  wrdexb  11379  sqr0lem  11656  rexanuz  11759  rexuz3  11762  fsum0diag  12170  sadcp1  12573  isprm6  12715  4sqlem4  12926  mreunirn  13430  isdrs2  14000  isacs5  14202  isacs4  14203  isacs3  14204  isnsg3  14578  gicer  14667  oppgmndb  14755  oppggrpb  14758  invghm  15057  opprrngb  15341  abvn0b  15970  gzrngunit  16364  zrngunit  16365  dvdsrz  16367  zlmlmod  16404  zlmassa  16405  cygth  16452  frgpcyg  16454  tgclb  16635  iscldtop  16759  isnrm2  17013  isnrm3  17014  discmp  17052  dfcon2  17072  2ndcsb  17102  dis2ndc  17113  loclly  17140  iskgen2  17170  dfac14  17239  kqtop  17363  kqt0  17364  kqreg  17369  kqnrm  17370  hmpher  17402  hmphsymb  17404  hmph0  17413  kqhmph  17437  ist1-5lem  17438  elmptrab2  17450  isfil2  17478  filunirn  17504  isufil2  17530  hausflim  17603  isfcls  17631  alexsubALT  17672  istgp2  17701  xmetunirn  17829  dscmet  18022  dscopn  18023  isngp4  18060  zcld  18246  zlmclm  18520  iscmet2  18647  iundisj  18832  i1f1lem  18971  fta1b  19482  elply2  19505  elqaa  19629  aannenlem2  19636  wilth  20236  lgsne0  20499  2sqlem2  20530  ostth  20715  nmlno0lem  21296  isblo3i  21304  blocni  21308  hvsubeq0i  21567  hvaddcani  21569  bcseqi  21624  isch3  21746  norm1exi  21754  hhsssh  21771  shslubi  21889  dfch2  21911  pjoc1i  21935  pjchi  21936  shs00i  21954  chsscon3i  21965  chlejb1i  21980  chj00i  21991  shjshseli  21997  h1de2ctlem  22059  spanunsni  22083  cmcmi  22114  cmbr3i  22122  cmbr4i  22123  pj11i  22233  hosubeq0i  22331  dmadjrnb  22411  nmlnop0iALT  22500  lnopeq0i  22512  elunop2  22518  lnconi  22538  lncnopbd  22542  adjbdlnb  22589  adjbd1o  22590  adjeq0  22596  rnbra  22612  pjss1coi  22668  pjss2coi  22669  pjnormssi  22673  pjssdif2i  22679  pjssdif1i  22680  dfpjop  22687  pjinvari  22696  pjin2i  22698  pjci  22705  pjcmul1i  22706  pjcmul2i  22707  strb  22763  hstrbi  22771  mdsl1i  22826  atom1d  22858  chrelat2i  22870  cvbr4i  22872  cvexchi  22874  sumdmdi  22925  dmdbr4ati  22926  dmdbr5ati  22927  dmdbr6ati  22928  dmdbr7ati  22929  cdj3i  22946  ballotlem2  22973  ballotlemrinv  23018  wrdumgra  23205  nepss  23409  dfpo2  23448  dfon2  23482  distel  23494  elno2  23641  axbday  23662  elfix  23784  dffix2  23786  fnimage  23808  altopthsn  23835  mptelee  23863  ellines  24115  rankeq1o  24141  df3nandALT1  24175  wl-pm5.74lem  24257  and4as  24270  altdftru  24279  trcrm  24282  facrm  24284  bibox  24313  binxt  24315  nxtor  24316  nxtand  24317  bidia  24320  evpexun  24329  alalifal  24334  boxand  24337  axlll2  24359  dmoprabss6  24366  restidsing  24407  fixpc  24425  sssu  24473  dstr  24503  definc  24611  domncnt  24614  ranncnt  24615  dfps2  24621  sallnei  24861  altretop  24932  addcanri  24998  bisig0  25394  opnrebl2  25568  locfindis  25637  cover2  25690  isbnd3  25840  cntotbnd  25852  heibor  25877  isfld2  25962  isfldidl  26025  prtlem16  26069  funsnfsup  26094  ismrc  26108  isnacs3  26117  rexzrexnn0  26217  eldioph4b  26226  dford3  26453  wopprc  26455  ttac  26461  pw2f1ocnv  26462  dfac11  26492  dfac21  26496  isnumbasabl  26603  isnumbasgrp  26604  dfacbasgrp  26605  aaitgo  26699  pmtrfb  26738  pm10.55  26896  pm11.57  26920  sbeqalbi  26932  pm13.192  26943  pm13.194  26945  ipo0  26985  ifr0  26986  xpexb  26991  com3rgbi  27292  pm2.43bgbi  27295  pm2.43cbi  27296  sb5ALT  27304  trsbc  27320  2pm13.193  27334  a9e2ndeq  27341  2uasbanh  27343  eelT01  27502  eel0T1  27503  uunT1  27568  zfregs2VD  27630  equncomVD  27657  trsbcVD  27666  undif3VD  27671  2pm13.193VD  27692  a9e2eqVD  27696  a9e2ndeqVD  27698  2uasbanhVD  27700  a9e2ndeqALT  27721  bnj1533  27896  bnj983  27995  albiiK  28122  19.8vK  28134  cbvalK  28141  cbvalvK  28142  ax12o10lem13K  28184  ax12o10lem13X  28185  ax12o10lem14K  28186  ax12o10lem14X  28187  equvinvK  28190  ax12olem16K  28191  ax12olem16X  28192  ax12olem17K  28193  ax12olem17X  28194  ax12olem21K  28201  ax12olem21X  28202  equextvK  28203  ax12olem23X  28207  ax12olem27X  28212  equvinv  28244  equvelv  28246  isltrn2N  29439
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