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

Theorem impbii 194
Description: Infer an equivalence from an implication and its converse. Inference associated with impbi 193. (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 193 . 2 ((𝜑𝜓) → ((𝜓𝜑) → (𝜑𝜓)))
41, 2, 3mp2 9 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 191
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 192
This theorem is referenced by:  dfbi1  198  bicom  207  biid  246  2th  249  pm5.74  254  bitri  259  notnotb  299  con34b  301  notbi  304  bibi2i  322  con1b  342  con2b  343  bi2.04  370  pm5.4  371  imdi  372  pm4.8  374  pm4.81  375  orcom  396  dfor2  420  impexp  455  ancom  459  oridm  529  orbi2i  534  or12  538  pm4.45im  577  pm4.44  593  pm4.79  599  anass  670  jaob  809  jcab  893  andi  897  pm4.72  906  oibabs  911  pm4.82  955  consensus  980  cases2  995  3impexp  1271  3jaob  1372  tbw-bijust  1611  tbw-negdf  1612  19.26  1763  19.35  1771  19.21v  1817  19.21vOLDOLD  1818  sbbii  1835  19.9v  1844  19.23v  1850  19.41v  1862  equcom  1894  equvinv  1908  equvinvOLD  1911  equvelv  1912  cbvalw  1916  alcom  1973  19.3  2019  19.41  2103  cbvalv1  2116  cbval  2161  equsex  2177  aecom  2194  equs45f  2233  dfsb2  2256  sb6f  2268  sbim  2278  sb6  2312  mo2v  2360  exmoeu  2385  mo3  2390  moanim  2412  euan  2413  2mo  2434  2eu6  2441  axext4  2489  eqcom  2512  nebi  2757  r19.26  2939  ralcom3  2977  ceqsex  3104  gencbvex  3113  gencbvex2  3114  eqvinc  3189  pm13.183  3202  rr19.3v  3203  rr19.28v  3204  euxfr2  3247  reu6  3251  reu3  3252  sspss  3554  complss  3599  unineq  3720  uneqin  3721  undif3  3731  difrab  3743  sbnfc2  3836  un00  3840  ssdifeq0  3877  r19.2zb  3886  ralf0  3903  elpr2  4017  snidb  4023  rabsnifsb  4068  tppreqb  4142  difsnb  4143  pwpw0  4149  sssn  4160  preq12b  4180  preqsn  4189  pwsnALT  4223  unissint  4288  uniintsn  4301  iununi  4397  intex  4597  intnex  4598  iin0  4615  axpweq  4618  eusvnfb  4638  eusv2nf  4640  ralxfrALT  4660  nfcvb  4671  sspwb  4690  unipw  4691  opnz  4714  opth  4717  opthwiener  4744  ssopab2b  4769  pwssun  4786  opelxp  4910  opthprc  4929  relop  5032  issetid  5036  xpid11  5105  elres  5190  eldmeldmressn  5195  iss  5202  restidsing  5211  issref  5263  asymref2  5267  xpnz  5306  xpdifid  5315  ssrnres  5325  dfrel2  5336  relrelss  5410  unixp0  5421  elon2  5485  fn0  5750  funssxp  5800  f00  5824  f0bi  5825  dffo2  5856  f1o00  5907  fo00  5908  fv3  5940  dffn5  5975  dff2  6101  dff3  6102  dffo4  6105  dffo5  6106  exfo  6107  fmpt  6110  ffnfv  6116  fsn  6129  fsn2  6130  fnsnb  6151  isores1  6298  ssoprab2b  6423  eqfnov2  6478  unexb  6668  uniexb  6678  iunpw  6682  ordeleqon  6692  onintrab  6705  unon  6735  onuninsuci  6744  ordzsl  6749  onzsl  6750  f1oexbi  6820  ffoss  6831  1st2ndb  6908  suppssov1  7025  suppssfv  7029  reldmtpos  7058  dfrecs3  7168  omopthi  7435  ecopover  7549  mapsn  7596  mapsncnv  7601  mptelixpg  7642  elixpsn  7644  ixpsnf1o  7645  bren2  7683  en0  7716  en1  7720  en1b  7721  sbthb  7777  canth2  7809  onfin2  7848  sdom1  7856  1sdom  7859  fineqv  7871  unfilem1  7920  fiint  7933  pwfi  7954  unifpw  7962  wofib  8143  sucprcreg  8199  opthreg  8208  suc11reg  8209  infeq5  8227  rankwflemb  8349  r1elss  8362  pwwf  8363  unwf  8366  uniwf  8375  rankonid  8385  rankr1id  8418  rankuni  8419  rankxplim3  8437  scott0  8442  karden  8451  isnum3  8473  oncard  8479  card1  8487  cardlim  8491  cardmin2  8517  pm54.43lem  8518  ween  8551  acnnum  8568  alephsuc2  8596  alephgeom  8598  iscard3  8609  dfac3  8637  dfac4  8638  dfac5lem3  8641  dfac5  8644  dfac2  8646  dfac8  8650  dfac9  8651  dfacacn  8656  dfac13  8657  dfac12r  8661  dfac12k  8662  kmlem2  8666  kmlem13  8677  cdainf  8707  ackbij2  8758  cflim2  8778  isfin4-2  8829  isfin4-3  8830  isf33lem  8881  compsscnv  8886  fin1a2lem6  8920  domtriom  8958  ac9  8998  ac9s  9008  fodomb  9039  brdom3  9041  brdom5  9042  brdom4  9043  brdom7disj  9044  brdom6disj  9045  iunfo  9049  sdomsdomcard  9070  gch2  9185  gch3  9186  eltsk2g  9261  grutsk  9332  grothpw  9336  ordpipq  9452  ltbtwnnq  9488  mappsrpr  9617  map2psrpr  9619  elreal2  9641  le2tri3i  9849  elnn0nn  11003  elnnnn0b  11005  elnnnn0c  11006  elnnz  11038  elnn0z  11041  elz2  11045  elnnz1  11054  eluz2b2  11322  elnn1uz2  11326  elioo4g  11790  eluzfz2b  11904  fzn0  11909  elfz1end  11925  fzass4  11933  elfz1b  11962  nn0fz0  11989  fzolb  12027  fzon0  12038  elfzo0  12058  elfzo0z  12059  elfzo1  12067  fzo1fzo0n0  12068  om2uzrani  12279  nn0opthi  12570  hashkf  12631  isfinite4  12661  hashprb  12692  hashf1  12743  elss2prb  12766  iswrdb  12805  wrdexb  12810  0wrd0  12825  wrdl3s3  13191  cotr2g  13198  trclun  13238  sqr0lem  13464  rexanuz  13568  rexuz3  13571  fsum0diag  13998  fprod0diag  14200  sadcp1  14591  isprm6  14828  4sqlem4  15058  mreunirn  15672  isdrs2  16350  isacs5  16583  isacs4  16584  isacs3  16585  isnsg3  17011  gicer  17100  gicerOLD  17101  oppgmndb  17167  oppggrpb  17170  pmtrfb  17267  invghm  17635  opprringb  18020  isnzr2hash  18647  abvn0b  18685  gzrngunit  19191  dvdsrzring  19210  zringunit  19220  zlmlmod  19252  zlmassa  19253  cygth  19300  frgpcyg  19302  tgclb  20143  iscldtop  20268  isnrm2  20531  isnrm3  20532  discmp  20570  dfcon2  20591  2ndcsb  20621  dis2ndc  20632  loclly  20659  unisngl  20699  locfindis  20702  iskgen2  20720  dfac14  20790  kqtop  20917  kqt0  20918  kqreg  20923  kqnrm  20924  hmpher  20956  hmphsymb  20958  hmph0  20967  kqhmph  20991  ist1-5lem  20992  elmptrab2OLD  21000  elmptrab2  21001  isfil2  21029  filunirn  21055  isufil2  21081  hausflim  21154  isfcls  21182  alexsubALT  21224  istgp2  21264  ustbas  21400  xmetunirn  21510  dscmet  21745  dscopn  21746  isngp4  21783  zcld  21989  zlmclm  22285  iscmet2  22423  iundisj  22661  i1f1lem  22808  fta1b  23281  elply2  23311  elqaa  23439  aannenlem2  23446  wilth  24157  lgsne0  24422  2sqlem2  24453  ostth  24638  mptelee  25086  uhgra0v  25198  wrdumgra  25204  usgra0v  25259  uvtx01vtx  25381  wlkcpr  25418  isspthonpth  25475  eclclwwlkn1  25720  usg2spthonot1  25778  clwlknclwlkdifs  25848  frgra0v  25881  nmlno0lem  26597  isblo3i  26605  blocni  26609  hvsubeq0i  26879  hvaddcani  26881  bcseqi  26936  isch3  27057  norm1exi  27066  hhsssh  27083  shslubi  27201  dfch2  27223  pjoc1i  27247  pjchi  27248  shs00i  27266  chsscon3i  27277  chlejb1i  27292  chj00i  27303  shjshseli  27309  h1de2ctlem  27371  spanunsni  27395  cmcmi  27408  cmbr3i  27416  cmbr4i  27417  pj11i  27527  hosubeq0i  27642  dmadjrnb  27722  nmlnop0iALT  27811  lnopeq0i  27823  elunop2  27829  lnconi  27849  lncnopbd  27853  adjbdlnb  27900  adjbd1o  27901  adjeq0  27907  rnbra  27923  pjss1coi  27979  pjss2coi  27980  pjnormssi  27984  pjssdif2i  27990  pjssdif1i  27991  dfpjop  27998  pjinvari  28007  pjin2i  28009  pjci  28016  pjcmul1i  28017  pjcmul2i  28018  strb  28074  hstrbi  28082  mdsl1i  28137  atom1d  28169  chrelat2i  28181  cvbr4i  28183  cvexchi  28185  sumdmdi  28236  dmdbr4ati  28237  dmdbr5ati  28238  dmdbr6ati  28239  dmdbr7ati  28240  cdj3i  28257  difeq  28312  iundisjf  28358  cnvoprab  28464  fpwrelmap  28474  iundisjfi  28528  xrge0tsmsbi  28704  issgon  29100  measbasedom  29179  oddpwdc  29341  eulerpartlemt  29358  ballotlem2  29475  ballotlemrinv  29520  ballotlemrinvOLD  29558  bnj1533  29815  bnj983  29914  elmsta  30338  nepss  30502  dfpo2  30546  dfon2  30589  distel  30601  elno2  30692  bdayfo  30715  fnimage  30847  altopthsn  30879  ellines  31070  rankeq1o  31089  opnrebl2  31126  df3nandALT1  31206  pm4.81ALT  31326  bj-dfbi6  31340  bj-consensus  31342  bj-falor2  31353  bj-bibibi  31354  bj-andnotim  31356  bj-ssbeq  31422  bj-ssb0  31423  bj-19.41al  31432  bj-sb56  31434  bj-eqs  31456  bj-cbvexw  31457  bj-sb  31465  bj-equs45fv  31544  bj-sbfvv  31559  bj-sb6  31562  bj-axext4  31567  bj-hbaeb2  31602  bj-hbnaeb  31604  bj-equsal  31610  bj-sbsb  31621  bj-mo3OLD  31631  bj-cleqhyp  31683  bj-csbsnlem  31689  bj-snsetex  31743  bj-snglex  31753  bj-1uplth  31787  bj-1uplex  31788  bj-2uplth  31801  bj-2uplex  31802  bj-restpw  31825  bj-restuni  31830  bj-elpw3  31836  bj-toprntopon  31843  bj-elid  31861  bj-elid3  31863  bj-eldiag2  31868  mptsnunlem  31961  topdifinf  31973  elxp8  31995  finxp1o  32005  wl-nfnbi  32091  wl-exeq  32098  wl-aleq  32099  wl-nfeqfb  32101  wl-ax11-lem6  32145  volsupnfl  32223  dvtanlemOLD  32229  cover2  32278  isbnd3  32353  cntotbnd  32365  heibor  32390  isfld2  32475  isfldidl  32538  orfa  32552  prtlem16  32674  isltrn2N  33925  ismrc  35783  isnacs3  35792  rexzrexnn0  35887  eldioph4b  35894  dford3  36123  wopprc  36125  ttac  36131  pw2f1ocnv  36132  dfac11  36160  dfac21  36164  isnumbasabl  36205  isnumbasgrp  36206  dfacbasgrp  36207  aaitgo  36268  ifpbi1b  36387  rp-fakeimass  36396  rp-fakeanorass  36397  rp-fakenanass  36399  rp-isfinite5  36402  rp-isfinite6  36403  rtrclex  36463  cnvtrrel  36501  rp-imass  36605  frege54cor0a  36698  isotone1  36872  isotone2  36873  gneispace  36930  k0004lem3  36945  nanorxor  37010  nzss  37023  pm10.55  37075  pm11.57  37096  sbeqalbi  37108  pm13.192  37118  pm13.194  37120  ipo0  37159  ifr0  37160  xpexb  37164  3impexpbicom  37191  com3rgbi  37227  pm2.43bgbi  37230  pm2.43cbi  37231  sb5ALT  37238  trsbc  37257  2pm13.193  37275  ax6e2ndeq  37282  2uasbanh  37284  eelT01  37444  eel0T1  37445  uunT1  37515  zfregs2VD  37585  equncomVD  37613  trsbcVD  37622  undif3VD  37627  2pm13.193VD  37648  ax6e2eqVD  37652  ax6e2ndeqVD  37654  2uasbanhVD  37656  ax6e2ndeqALT  37676  fompt  37827  elfzfzo  37865  dvnprodlem3  38242  elaa2  38535  sge00  38664  ismea  38739  elhoi  38827  ovn0  38851  ovolval4lem2  38935  confun  39047  reuan  39121  afvfv0bi  39174  ffnafv  39193  clel5  39503  propeqop  39521  funop  39540  funsneqopb  39546  residfi  39562  wrdupgr  39711  wrdumgr  39722  umgrislfupgr  39748  uspgrupgrushgr  39807  usgrumgruspgr  39810  usgruspgrb  39811  usgrislfuspgr  39814  uvtxa01vtx0  40023  isclWlkb  40380  clwwlknclwwlkdifs  40581  eclclwwlksn1  40659  upgriseupth  40775  mgm2mgm  41053  isringrng  41071  nnpw2pb  41587
  Copyright terms: Public domain W3C validator