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

Theorem impbii 197
Description: Infer an equivalence from an implication and its converse. Inference associated with impbi 196. (Contributed by NM, 29-Dec-1992.)
Hypotheses
Ref Expression
impbii.1 (𝜑𝜓)
impbii.2 (𝜓𝜑)
Assertion
Ref Expression
impbii (𝜑𝜓)

Proof of Theorem impbii
StepHypRef Expression
1 impbii.1 . 2 (𝜑𝜓)
2 impbii.2 . 2 (𝜓𝜑)
3 impbi 196 . 2 ((𝜑𝜓) → ((𝜓𝜑) → (𝜑𝜓)))
41, 2, 3mp2 9 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  dfbi1  201  bicom  210  biid  249  2th  252  pm5.74  257  bitri  262  notnotb  302  con34b  304  notbi  307  bibi2i  325  con1b  346  con2b  347  bi2.04  374  pm5.4  375  imdi  376  pm4.8  378  pm4.81  379  orcom  400  biorfi  420  dfor2  425  impexp  460  ancom  464  oridm  534  orbi2i  539  or12  543  pm4.45im  582  pm4.44  598  pm4.79  604  anass  678  jaob  817  jcab  902  andi  906  pm4.72  915  oibabs  920  pm4.82  964  consensus  989  cases2  1004  3impexp  1280  3jaob  1381  tbw-bijust  1613  tbw-negdf  1614  19.26  1767  19.35  1775  19.21v  1821  sbbii  1837  19.9v  1846  19.23v  1852  19.41v  1864  equcom  1895  equvinv  1909  equvinvOLD  1912  equvelv  1913  cbvalw  1917  alcom  1974  19.3  2018  19.41  2101  cbvalv1  2115  cbval  2162  cbvalv  2164  equsex  2184  aecom  2203  equs45f  2242  dfsb2  2265  sb6f  2277  sbim  2287  sb6  2321  mo2v  2369  exmoeu  2394  mo3  2399  moanim  2421  euan  2422  2mo  2443  2eu6  2450  axext4  2498  eqcom  2521  nebi  2766  r19.26  2950  ralcom3  2988  ceqsex  3118  gencbvex  3127  gencbvex2  3128  eqvinc  3204  pm13.183  3217  rr19.3v  3218  rr19.28v  3219  euxfr2  3262  reu6  3266  reu3  3267  sspss  3572  complss  3617  unineq  3739  uneqin  3740  undif3OLD  3751  difrab  3763  sbnfc2  3862  un00  3866  ssdifeq0  3906  r19.2zb  3916  ralf0OLD  3934  elpr2OLD  4051  snidb  4057  rabsnifsb  4104  tppreqb  4180  difsnb  4181  pwpw0  4187  sssn  4199  preq12b  4221  preqsnOLD  4231  pwsnALT  4265  unissint  4334  uniintsn  4347  iununi  4444  intex  4646  intnex  4647  iin0  4664  axpweq  4667  eusvnfb  4687  eusv2nf  4689  ralxfrALT  4712  nfcvb  4723  sspwb  4742  unipw  4743  opnz  4766  opth  4769  opthwiener  4796  ssopab2b  4821  pwssun  4838  opelxp  4964  opthprc  4983  relop  5086  issetid  5090  xpid11  5159  elres  5246  eldmeldmressn  5251  iss  5258  restidsingOLD  5269  issref  5319  asymref2  5323  xpnz  5362  xpdifid  5371  ssrnres  5381  dfrel2  5392  relrelss  5466  unixp0  5476  fn0  5814  funssxp  5864  f00  5889  f0bi  5890  dffo2  5921  f1o00  5972  fo00  5973  fv3  6005  dffn5  6040  dff2  6168  dff3  6169  dffo4  6172  dffo5  6173  exfo  6174  fmpt  6178  ffnfv  6184  fsn  6197  fsn2  6198  fnsnb  6219  isores1  6366  ssoprab2b  6492  eqfnov2  6547  unexb  6737  uniexb  6747  iunpw  6751  ordeleqon  6761  onintrab  6774  unon  6804  onuninsuci  6813  ordzsl  6818  onzsl  6819  f1oexbi  6889  ffoss  6900  1st2ndb  6977  suppssov1  7094  suppssfv  7098  reldmtpos  7127  dfrecs3  7236  omopthi  7504  ecopover  7618  mapsn  7665  mapsncnv  7670  mptelixpg  7711  elixpsn  7713  ixpsnf1o  7714  bren2  7752  en0  7785  en1  7789  en1b  7790  sbthb  7846  canth2  7878  onfin2  7917  sdom1  7925  1sdom  7928  fineqv  7940  unfilem1  7989  fiint  8002  pwfi  8024  unifpw  8032  wofib  8213  sucprcreg  8269  opthreg  8278  suc11reg  8279  infeq5  8297  rankwflemb  8419  r1elss  8432  pwwf  8433  unwf  8436  uniwf  8445  rankonid  8455  rankr1id  8488  rankuni  8489  rankxplim3  8507  scott0  8512  karden  8521  isnum3  8543  oncard  8549  card1  8557  cardlim  8561  cardmin2  8587  pm54.43lem  8588  ween  8621  acnnum  8638  alephsuc2  8666  alephgeom  8668  iscard3  8679  dfac3  8707  dfac4  8708  dfac5lem3  8711  dfac5  8714  dfac2  8716  dfac8  8720  dfac9  8721  dfacacn  8726  dfac13  8727  dfac12r  8731  dfac12k  8732  kmlem2  8736  kmlem13  8747  cdainf  8777  ackbij2  8828  cflim2  8848  isfin4-2  8899  isfin4-3  8900  isf33lem  8951  compsscnv  8956  fin1a2lem6  8990  domtriom  9028  ac9  9068  ac9s  9078  fodomb  9109  brdom3  9111  brdom5  9112  brdom4  9113  brdom7disj  9114  brdom6disj  9115  iunfo  9120  sdomsdomcard  9141  gch2  9256  gch3  9257  eltsk2g  9332  grutsk  9403  grothpw  9407  ordpipq  9523  ltbtwnnq  9559  mappsrpr  9688  map2psrpr  9690  elreal2  9712  le2tri3i  9922  elnn0nn  11094  elnnnn0b  11096  elnnnn0c  11097  elnnz  11132  elnn0z  11135  elz2  11139  elnnz1  11148  eluz2b2  11505  elnn1uz2  11509  elioo4g  11978  eluzfz2b  12093  fzn0  12098  elfz1end  12114  fzass4  12122  elfz1b  12151  nn0fz0  12178  fzolb  12217  fzon0  12228  elfzo0  12248  elfzo0z  12249  elfzo1  12257  fzo1fzo0n0  12258  om2uzrani  12485  nn0opthi  12791  hashkf  12853  isfinite4  12883  hashprb  12915  hashf1  12967  elss2prb  12990  iswrdb  13029  wrdexb  13034  0wrd0  13049  wrdl3s3  13416  cotr2g  13426  trclun  13466  sqr0lem  13692  rexanuz  13796  rexuz3  13799  fsum0diag  14224  fprod0diag  14429  divalgmod  14843  sadcp1  14892  isprm6  15144  nnoddn2prmb  15244  4sqlem4  15382  mreunirn  15980  isdrs2  16658  isacs5  16891  isacs4  16892  isacs3  16893  dfgrp2  17166  dfgrp3  17233  dfgrp3e  17234  isnsg3  17347  gicer  17437  gicerOLD  17438  oppgmndb  17504  oppggrpb  17507  pmtrfb  17604  invghm  17973  opprringb  18366  isnzr2hash  18993  abvn0b  19031  gzrngunit  19539  dvdsrzring  19558  zringunit  19568  zlmlmod  19600  zlmassa  19601  cygth  19649  frgpcyg  19651  tgclb  20492  iscldtop  20616  isnrm2  20879  isnrm3  20880  discmp  20918  dfcon2  20939  2ndcsb  20969  dis2ndc  20980  loclly  21007  unisngl  21047  locfindis  21050  iskgen2  21068  dfac14  21138  kqtop  21265  kqt0  21266  kqreg  21271  kqnrm  21272  hmpher  21304  hmphsymb  21306  hmph0  21315  kqhmph  21339  ist1-5lem  21340  elmptrab2OLD  21348  elmptrab2  21349  isfil2  21377  filunirn  21403  isufil2  21429  hausflim  21502  isfcls  21530  alexsubALT  21572  istgp2  21612  ustbas  21748  xmetunirn  21858  dscmet  22093  dscopn  22094  isngp4  22131  zcld  22337  zlmclm  22630  iscmet2  22768  iundisj  23002  i1f1lem  23141  fta1b  23614  elply2  23644  elqaa  23772  aannenlem2  23779  wilth  24488  lgsne0  24753  2lgs  24825  2sqlem2  24836  ostth  25021  mptelee  25469  uhgra0v  25581  wrdumgra  25587  usgra0v  25642  uvtx01vtx  25762  wlkcpr  25799  isspthonpth  25856  eclclwwlkn1  26101  usg2spthonot1  26159  clwlknclwlkdifs  26229  frgra0v  26262  nmlno0lem  26814  isblo3i  26822  blocni  26826  hvsubeq0i  27096  hvaddcani  27098  bcseqi  27153  isch3  27274  norm1exi  27283  hhsssh  27302  shslubi  27420  dfch2  27442  pjoc1i  27466  pjchi  27467  shs00i  27485  chsscon3i  27496  chlejb1i  27511  chj00i  27522  shjshseli  27528  h1de2ctlem  27590  spanunsni  27614  cmcmi  27627  cmbr3i  27635  cmbr4i  27636  pj11i  27746  hosubeq0i  27861  dmadjrnb  27941  nmlnop0iALT  28030  lnopeq0i  28042  elunop2  28048  lnconi  28068  lncnopbd  28072  adjbdlnb  28119  adjbd1o  28120  adjeq0  28126  rnbra  28142  pjss1coi  28198  pjss2coi  28199  pjnormssi  28203  pjssdif2i  28209  pjssdif1i  28210  dfpjop  28217  pjinvari  28226  pjin2i  28228  pjci  28235  pjcmul1i  28236  pjcmul2i  28237  strb  28293  hstrbi  28301  mdsl1i  28356  atom1d  28388  chrelat2i  28400  cvbr4i  28402  cvexchi  28404  sumdmdi  28455  dmdbr4ati  28456  dmdbr5ati  28457  dmdbr6ati  28458  dmdbr7ati  28459  cdj3i  28476  difeq  28531  iundisjf  28576  cnvoprab  28678  fpwrelmap  28688  iundisjfi  28741  xrge0tsmsbi  28917  issgon  29313  measbasedom  29392  oddpwdc  29554  eulerpartlemt  29571  ballotlem2  29688  ballotlemrinv  29733  ballotlemrinvOLD  29771  bnj1533  30025  bnj983  30124  elmsta  30548  nepss  30701  dfpo2  30744  dfon2  30787  distel  30799  elno2  30890  bdayfo  30913  fnimage  31045  altopthsn  31077  ellines  31268  rankeq1o  31287  opnrebl2  31324  df3nandALT1  31404  pm4.81ALT  31554  bj-dfbi6  31568  bj-consensus  31570  bj-falor2  31581  bj-bibibi  31582  bj-andnotim  31584  bj-ssbeq  31654  bj-ssb0  31655  bj-19.41al  31664  bj-sb56  31666  bj-eqs  31688  bj-cbvexw  31689  bj-sb  31702  bj-equs45fv  31780  bj-sbfvv  31795  bj-sb6  31798  bj-axext4  31803  bj-hbaeb2  31838  bj-hbnaeb  31840  bj-equsal  31846  bj-sbsb  31857  bj-mo3OLD  31867  bj-cleqhyp  31919  bj-csbsnlem  31925  bj-snsetex  31979  bj-snglex  31989  bj-1uplth  32023  bj-1uplex  32024  bj-2uplth  32037  bj-2uplex  32038  bj-restpw  32061  bj-restuni  32066  bj-elpw3  32072  bj-toprntopon  32079  bj-elid  32097  bj-elid3  32099  bj-eldiag2  32104  mptsnunlem  32196  topdifinf  32208  elxp8  32230  finxp1o  32240  wl-nfnbi  32386  wl-exeq  32393  wl-aleq  32394  wl-nfeqfb  32396  wl-ax11-lem6  32440  volsupnfl  32518  cover2  32572  isbnd3  32647  cntotbnd  32659  heibor  32684  isfld2  32868  isfldidl  32931  orfa  32945  prtlem16  33066  isltrn2N  34318  ismrc  36176  isnacs3  36185  rexzrexnn0  36280  eldioph4b  36287  dford3  36507  wopprc  36509  ttac  36515  pw2f1ocnv  36516  dfac11  36544  dfac21  36548  isnumbasabl  36589  isnumbasgrp  36590  dfacbasgrp  36591  aaitgo  36652  ifpbi1b  36768  rp-fakeimass  36777  rp-fakeanorass  36778  rp-fakenanass  36780  rp-isfinite5  36783  rp-isfinite6  36784  rtrclex  36844  cnvtrrel  36882  rp-imass  36986  frege54cor0a  37078  isotone1  37267  isotone2  37268  gneispace  37353  k0004lem3  37368  nanorxor  37427  nzss  37439  pm10.55  37491  pm11.57  37512  sbeqalbi  37524  pm13.192  37534  pm13.194  37536  ipo0  37575  ifr0  37576  xpexb  37580  3impexpbicom  37607  com3rgbi  37642  pm2.43bgbi  37645  pm2.43cbi  37646  sb5ALT  37653  trsbc  37672  2pm13.193  37690  ax6e2ndeq  37697  2uasbanh  37699  eelT01  37858  eel0T1  37859  uunT1  37929  zfregs2VD  37999  equncomVD  38027  trsbcVD  38036  undif3VD  38041  2pm13.193VD  38062  ax6e2eqVD  38066  ax6e2ndeqVD  38068  2uasbanhVD  38070  ax6e2ndeqALT  38090  fompt  38276  elfzfzo  38331  allbutfi  38460  dvnprodlem3  38745  elaa2  39037  sge00  39180  ismea  39255  elhoi  39343  ovn0  39367  ovolval4lem2  39451  confun  39666  reuan  39740  afvfv0bi  39793  ffnafv  39812  clel5  40215  propeqop  40233  funop  40252  funsneqopb  40258  residfi  40274  wrdupgr  40420  wrdumgr  40431  umgrislfupgr  40457  uspgrupgrushgr  40516  usgrumgruspgr  40519  usgruspgrb  40520  usgrislfuspgr  40523  uvtxa01vtx0  40732  isclWlkb  41089  clwwlknclwwlkdifs  41290  eclclwwlksn1  41368  upgriseupth  41484  mgm2mgm  41762  isringrng  41780  nnpw2pb  42288
  Copyright terms: Public domain W3C validator