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

Theorem impbii 199
Description: Infer an equivalence from an implication and its converse. Inference associated with impbi 198. (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 198 . 2 ((𝜑𝜓) → ((𝜓𝜑) → (𝜑𝜓)))
41, 2, 3mp2 9 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  dfbi1  203  bicom  212  biid  251  2th  254  pm5.74  259  bitri  264  notnotb  304  con34b  306  notbi  309  bibi2i  327  con1b  348  con2b  349  bi2.04  376  pm5.4  377  imdi  378  pm4.8  380  pm4.81  381  orcom  402  biorfi  422  dfor2  427  impexp  462  ancom  466  oridm  536  orbi2i  541  or12  545  pm4.45im  585  pm4.44  601  pm4.79  607  anass  681  jaob  822  jcab  907  andi  911  pm4.72  920  oibabs  925  pm4.82  969  cases2  993  consensus  999  3impexp  1288  3jaob  1389  tbw-bijust  1622  tbw-negdf  1623  19.26  1797  19.35  1804  19.21v  1867  sbbii  1886  19.9v  1895  19.23v  1901  19.41v  1913  equcom  1944  equvinv  1958  equvinvOLD  1961  equvelv  1962  cbvalw  1967  alcom  2036  19.3  2068  19.41  2102  cbvalv1  2174  19.3OLD  2201  cbval  2270  cbvalv  2272  equsex  2291  aecom  2310  equs45f  2349  dfsb2  2372  sb6f  2384  sbim  2394  sb6  2428  mo2v  2476  exmoeu  2501  mo3  2506  moanim  2528  euan  2529  2mo  2550  2eu6  2557  axext4  2605  eqcom  2628  nebi  2873  r19.26  3062  ralcom3  3103  ceqsex  3239  gencbvex  3248  gencbvex2  3249  clel5  3341  pm13.183  3342  rr19.3v  3343  rr19.28v  3344  euxfr2  3389  reu6  3393  reu3  3394  sspss  3704  complss  3749  unineq  3875  uneqin  3876  undif3OLD  3887  difrab  3899  sbnfc2  4005  un00  4009  ssdifeq0  4049  r19.2zb  4059  ralf0OLD  4077  elpr2OLD  4198  snidb  4205  rabsnifsb  4255  ssdifsn  4316  tppreqb  4334  difsnb  4335  pwpw0  4342  sssn  4356  preq12b  4380  preqsnOLD  4392  pwsnALT  4427  unissint  4499  uniintsn  4512  iununi  4608  intex  4818  intnex  4819  iin0  4837  axpweq  4840  eusvnfb  4860  eusv2nf  4862  ralxfrALT  4885  nfcvb  4896  sspwb  4915  unipw  4916  opnz  4940  opth  4943  propeqop  4968  opthwiener  4974  ssopab2b  5000  pwssun  5018  opelxp  5144  opthprc  5165  relop  5270  issetid  5274  xpid11  5345  elres  5433  eldmeldmressn  5438  iss  5445  restidsingOLD  5457  issref  5507  asymref2  5511  xpnz  5551  xpdifid  5560  ssrnres  5570  dfrel2  5581  relrelss  5657  unixp0  5667  fn0  6009  funssxp  6059  f00  6085  f0bi  6086  dffo2  6117  f1o00  6169  fo00  6170  fv3  6204  dffn5  6239  dff2  6369  dff3  6370  dffo4  6373  dffo5  6374  exfo  6375  fmpt  6379  ffnfv  6386  fsn  6399  fsn2  6400  funop  6411  funsneqopb  6416  fnsnb  6429  isores1  6581  ssoprab2b  6709  eqfnov2  6764  unexb  6955  uniexb  6970  pwexb  6972  iunpw  6975  ordeleqon  6985  onintrab  6998  unon  7028  onuninsuci  7037  ordzsl  7042  onzsl  7043  f1oexbi  7113  ffoss  7124  1st2ndb  7203  suppssov1  7324  suppssfv  7328  reldmtpos  7357  dfrecs3  7466  omopthi  7734  ecopover  7848  mapsn  7896  mapsncnv  7901  mptelixpg  7942  elixpsn  7944  ixpsnf1o  7945  bren2  7983  en0  8016  en1  8020  en1b  8021  sbthb  8078  canth2  8110  onfin2  8149  sdom1  8157  1sdom  8160  fineqv  8172  unfilem1  8221  fiint  8234  residfi  8244  pwfi  8258  unifpw  8266  wofib  8447  sucprcreg  8503  opthreg  8512  suc11reg  8513  infeq5  8531  rankwflemb  8653  r1elss  8666  pwwf  8667  unwf  8670  uniwf  8679  rankonid  8689  rankr1id  8722  rankuni  8723  rankxplim3  8741  scott0  8746  karden  8755  isnum3  8777  oncard  8783  card1  8791  cardlim  8795  cardmin2  8821  pm54.43lem  8822  ween  8855  acnnum  8872  alephsuc2  8900  alephgeom  8902  iscard3  8913  dfac3  8941  dfac4  8942  dfac5lem3  8945  dfac5  8948  dfac2  8950  dfac8  8954  dfac9  8955  dfacacn  8960  dfac13  8961  dfac12r  8965  dfac12k  8966  kmlem2  8970  kmlem13  8981  cdainf  9011  ackbij2  9062  cflim2  9082  isfin4-2  9133  isfin4-3  9134  isf33lem  9185  compsscnv  9190  fin1a2lem6  9224  domtriom  9262  ac9  9302  ac9s  9312  fodomb  9345  brdom3  9347  brdom5  9348  brdom4  9349  brdom7disj  9350  brdom6disj  9351  iunfo  9358  sdomsdomcard  9379  gch2  9494  gch3  9495  eltsk2g  9570  grutsk  9641  grothpw  9645  ordpipq  9761  ltbtwnnq  9797  mappsrpr  9926  map2psrpr  9928  elreal2  9950  le2tri3i  10164  elnn0nn  11332  elnnnn0b  11334  elnnnn0c  11335  elnnz  11384  elnn0z  11387  elz2  11391  elnnz1  11400  eluz2b2  11758  elnn1uz2  11762  elioo4g  12231  eluzfz2b  12347  fzn0  12352  elfz1end  12368  fzass4  12376  elfz1b  12406  nn0fz0  12433  fzolb  12472  fzon0  12483  elfzo0  12504  elfzo0z  12505  elfzo1  12513  fzo1fzo0n0  12514  om2uzrani  12746  nn0opthi  13052  hashkf  13114  isfinite4  13148  hashprb  13180  hashf1  13236  elss2prb  13264  iswrdb  13306  wrdexb  13311  0wrd0  13326  wrdl3s3  13699  cotr2g  13709  trclun  13749  sqr0lem  13975  rexanuz  14079  rexuz3  14082  fsum0diag  14503  fprod0diag  14711  divalgmod  15123  sadcp1  15171  isprm6  15420  nnoddn2prmb  15512  4sqlem4  15650  mreunirn  16255  isdrs2  16933  isacs5  17166  isacs4  17167  isacs3  17168  dfgrp2  17441  dfgrp3  17508  dfgrp3e  17509  isnsg3  17622  gicer  17712  gicerOLD  17713  oppgmndb  17779  oppggrpb  17782  pmtrfb  17879  invghm  18233  opprringb  18626  isnzr2hash  19258  abvn0b  19296  gzrngunit  19806  dvdsrzring  19825  zringunit  19830  zlmlmod  19865  zlmassa  19866  cygth  19914  frgpcyg  19916  toprntopon  20723  tgclb  20768  iscldtop  20893  isnrm2  21156  isnrm3  21157  discmp  21195  dfconn2  21216  2ndcsb  21246  dis2ndc  21257  loclly  21284  unisngl  21324  locfindis  21327  iskgen2  21345  dfac14  21415  kqtop  21542  kqt0  21543  kqreg  21548  kqnrm  21549  hmpher  21581  hmphsymb  21583  hmph0  21592  kqhmph  21616  ist1-5lem  21617  elmptrab2OLD  21625  elmptrab2  21626  isfil2  21654  filunirn  21680  isufil2  21706  hausflim  21779  isfcls  21807  alexsubALT  21849  istgp2  21889  ustbas  22025  xmetunirn  22136  dscmet  22371  dscopn  22372  isngp4  22410  zcld  22610  zlmclm  22906  iscmet2  23086  iundisj  23310  i1f1lem  23450  fta1b  23923  elply2  23946  elqaa  24071  aannenlem2  24078  wilth  24791  lgsne0  25054  2lgs  25126  2sqlem2  25137  ostth  25322  mptelee  25769  wrdupgr  25974  wrdumgr  25986  umgrislfupgr  26012  uspgrupgrushgr  26066  usgrumgruspgr  26069  usgruspgrb  26070  usgrislfuspgr  26073  uvtxa01vtx0  26291  clwwlknclwwlkdifs  26867  eclclwwlksn1  26945  upgriseupth  27060  nmlno0lem  27632  isblo3i  27640  blocni  27644  hvsubeq0i  27904  hvaddcani  27906  bcseqi  27961  isch3  28082  norm1exi  28091  hhsssh  28110  shslubi  28228  dfch2  28250  pjoc1i  28274  pjchi  28275  shs00i  28293  chsscon3i  28304  chlejb1i  28319  chj00i  28330  shjshseli  28336  h1de2ctlem  28398  spanunsni  28422  cmcmi  28435  cmbr3i  28443  cmbr4i  28444  pj11i  28554  hosubeq0i  28669  dmadjrnb  28749  nmlnop0iALT  28838  lnopeq0i  28850  elunop2  28856  lnconi  28876  lncnopbd  28880  adjbdlnb  28927  adjbd1o  28928  adjeq0  28934  rnbra  28950  pjss1coi  29006  pjss2coi  29007  pjnormssi  29011  pjssdif2i  29017  pjssdif1i  29018  dfpjop  29025  pjinvari  29034  pjin2i  29036  pjci  29043  pjcmul1i  29044  pjcmul2i  29045  strb  29101  hstrbi  29109  mdsl1i  29164  atom1d  29196  chrelat2i  29208  cvbr4i  29210  cvexchi  29212  sumdmdi  29263  dmdbr4ati  29264  dmdbr5ati  29265  dmdbr6ati  29266  dmdbr7ati  29267  cdj3i  29284  difeq  29339  iundisjf  29386  cnvoprab  29483  fpwrelmap  29493  iundisjfi  29540  xrge0tsmsbi  29771  issgon  30171  measbasedom  30250  oddpwdc  30401  eulerpartlemt  30418  ballotlem2  30535  ballotlemrinv  30580  bnj1533  30907  bnj983  31006  elmsta  31430  nepss  31585  dford5  31594  dfpo2  31631  dfon2  31681  distel  31693  elno2  31791  bdayfo  31812  fnimage  32020  altopthsn  32052  ellines  32243  rankeq1o  32262  opnrebl2  32300  df3nandALT1  32380  pm4.81ALT  32530  bj-dfbi6  32544  bj-consensus  32546  bj-falor2  32554  bj-bibibi  32555  bj-andnotim  32557  bj-ssbeq  32611  bj-ssb0  32612  bj-19.41al  32621  bj-sb56  32623  bj-eqs  32647  bj-cbvexw  32648  bj-sb  32661  bj-equs45fv  32736  bj-sbfvv  32749  bj-sb6  32751  bj-axext4  32754  bj-hbaeb2  32789  bj-hbnaeb  32791  bj-equsal  32797  bj-sbsb  32808  bj-mo3OLD  32816  bj-cleqhyp  32876  bj-csbsnlem  32882  bj-snsetex  32935  bj-snglex  32945  bj-1uplth  32979  bj-1uplex  32980  bj-2uplth  32993  bj-2uplex  32994  bj-restpw  33029  bj-restuni  33034  bj-ismooredr2  33049  bj-discrmoore  33050  bj-snmoore  33052  bj-elid  33065  bj-elid3  33067  bj-eldiag2  33072  mptsnunlem  33165  topdifinf  33177  elxp8  33199  finxp1o  33209  wl-nfnbi  33294  wl-exeq  33301  wl-aleq  33302  wl-nfeqfb  33303  wl-ax11-lem6  33347  volsupnfl  33434  cover2  33488  isbnd3  33563  cntotbnd  33575  heibor  33600  isfld2  33784  isfldidl  33847  orfa  33861  prtlem16  33980  isltrn2N  35232  ismrc  37090  isnacs3  37099  rexzrexnn0  37194  eldioph4b  37201  dford3  37421  wopprc  37423  ttac  37429  pw2f1ocnv  37430  dfac11  37458  dfac21  37462  isnumbasabl  37502  isnumbasgrp  37503  dfacbasgrp  37504  aaitgo  37558  ifpbi1b  37674  rp-fakeimass  37683  rp-fakeanorass  37684  rp-fakenanass  37686  rp-isfinite5  37689  rp-isfinite6  37690  rtrclex  37750  cnvtrrel  37788  rp-imass  37891  frege54cor0a  37983  isotone1  38172  isotone2  38173  gneispace  38258  k0004lem3  38273  nanorxor  38330  nzss  38342  pm10.55  38394  pm11.57  38415  sbeqalbi  38427  pm13.192  38437  pm13.194  38439  ipo0  38479  ifr0  38480  xpexb  38484  3impexpbicom  38511  com3rgbi  38546  pm2.43bgbi  38549  pm2.43cbi  38550  sb5ALT  38557  trsbc  38576  2pm13.193  38594  ax6e2ndeq  38601  2uasbanh  38603  eelT01  38762  eel0T1  38763  uunT1  38833  zfregs2VD  38902  equncomVD  38930  trsbcVD  38939  undif3VD  38944  2pm13.193VD  38965  ax6e2eqVD  38969  ax6e2ndeqVD  38971  2uasbanhVD  38973  ax6e2ndeqALT  38993  fompt  39201  mptssid  39272  elfzfzo  39307  allbutfi  39435  uzn0bi  39508  dvnprodlem3  39932  elaa2  40220  sge00  40362  ismea  40437  elhoi  40525  ovn0  40549  ovolval4lem2  40633  confun  40875  reuan  40949  afvfv0bi  41001  ffnafv  41020  sbgoldbmb  41445  mgm2mgm  41634  isringrng  41652  nnpw2pb  42152  elsetrecs  42216  elpg  42228
  Copyright terms: Public domain W3C validator