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  305  notbi  308  bibi2i  326  con1b  347  con2b  348  bi2.04  375  pm5.4  376  imdi  377  pm4.8  379  pm4.81  380  orcom  401  biorfi  421  dfor2  426  impexp  461  ancom  465  oridm  535  orbi2i  540  or12  544  pm4.45im  584  pm4.44  600  pm4.79  606  anass  682  jaob  839  jcab  925  andi  929  pm4.72  938  oibabs  943  annotanannotOLD  960  pm4.82  989  cases2ALT  1017  consensus  1023  3impexp  1311  3jaob  1430  tbw-bijust  1663  tbw-negdf  1664  19.26  1838  19.35  1845  19.21v  1908  19.23v  1911  19.41v  1917  sbbii  1944  19.9v  1953  19.23vOLD  1959  19.41vOLD  1970  equcom  1991  equvinv  2003  equvelv  2005  cbvalw  2010  alcom  2077  19.3  2107  19.41  2141  cbvalv1  2211  19.3OLD  2238  cbval  2307  cbvalv  2309  equsex  2328  aecom  2344  equs45f  2378  dfsb2  2401  sb6f  2413  sbim  2423  sb6  2457  mo2v  2505  exmoeu  2531  mo3  2536  moanim  2558  euan  2559  2mo  2580  2eu6  2587  axext4  2635  eqcom  2658  nebi  2903  r19.26  3093  ralcom3  3134  ceqsex  3272  gencbvex  3281  gencbvex2  3282  clel5  3375  pm13.183  3376  rr19.3v  3377  rr19.28v  3378  euxfr2  3424  reu6  3428  reu3  3429  sspss  3739  complss  3784  unineq  3910  uneqin  3911  undif3OLD  3922  difrab  3934  sbnfc2  4040  un00  4044  ssdifeq0  4084  r19.2zb  4094  ralf0OLD  4112  elpr2OLD  4233  snidb  4240  rabsnifsb  4289  ssdifsn  4351  tppreqb  4368  difsnb  4369  pwpw0  4376  sssn  4390  preq12b  4413  preqsnOLD  4425  pwsnALT  4461  unissint  4533  uniintsn  4546  iununi  4642  intex  4850  intnex  4851  iin0  4869  axpweq  4872  eusvnfb  4892  eusv2nf  4894  ralxfrALT  4917  nfcvb  4928  sspwb  4947  unipw  4948  opnz  4971  opth  4974  propeqop  4999  opthwiener  5005  ssopab2b  5031  pwssun  5049  opelxp  5180  opthprc  5201  relop  5305  issetid  5309  xpid11  5379  elres  5470  eldmeldmressn  5475  iss  5482  restidsingOLD  5494  issref  5544  asymref2  5548  xpnz  5588  xpdifid  5597  ssrnres  5607  dfrel2  5618  relrelss  5697  unixp0  5707  fn0  6049  funssxp  6099  f00  6125  f0bi  6126  dffo2  6157  f1o00  6209  fo00  6210  fv3  6244  dffn5  6280  dff2  6411  dff3  6412  dffo4  6415  dffo5  6416  exfo  6417  fmpt  6421  ffnfv  6428  fsn  6442  fsn2  6443  funop  6454  funsneqopb  6459  fnsnb  6473  isores1  6624  ssoprab2b  6754  eqfnov2  6809  unexb  7000  uniexb  7015  pwexb  7017  iunpw  7020  ordeleqon  7030  onintrab  7043  unon  7073  onuninsuci  7082  ordzsl  7087  onzsl  7088  f1oexbi  7158  ffoss  7169  1st2ndb  7250  suppssov1  7372  suppssfv  7376  reldmtpos  7405  dfrecs3  7514  omopthi  7782  ecopover  7894  mapsn  7941  mapsncnv  7946  mptelixpg  7987  elixpsn  7989  ixpsnf1o  7990  bren2  8028  en0  8060  en1  8064  en1b  8065  sbthb  8122  canth2  8154  onfin2  8193  sdom1  8201  1sdom  8204  fineqv  8216  unfilem1  8265  fiint  8278  residfi  8288  pwfi  8302  unifpw  8310  wofib  8491  sucprcreg  8544  opthreg  8553  suc11reg  8554  infeq5  8572  rankwflemb  8694  r1elss  8707  pwwf  8708  unwf  8711  uniwf  8720  rankonid  8730  rankr1id  8763  rankuni  8764  rankxplim3  8782  scott0  8787  karden  8796  isnum3  8818  oncard  8824  card1  8832  cardlim  8836  cardmin2  8862  pm54.43lem  8863  ween  8896  acnnum  8913  alephsuc2  8941  alephgeom  8943  iscard3  8954  dfac3  8982  dfac4  8983  dfac5lem3  8986  dfac5  8989  dfac2  8991  dfac8  8995  dfac9  8996  dfacacn  9001  dfac13  9002  dfac12r  9006  dfac12k  9007  kmlem2  9011  kmlem13  9022  cdainf  9052  ackbij2  9103  cflim2  9123  isfin4-2  9174  isfin4-3  9175  isf33lem  9226  compsscnv  9231  fin1a2lem6  9265  domtriom  9303  ac9  9343  ac9s  9353  fodomb  9386  brdom3  9388  brdom5  9389  brdom4  9390  brdom7disj  9391  brdom6disj  9392  iunfo  9399  sdomsdomcard  9420  gch2  9535  gch3  9536  eltsk2g  9611  grutsk  9682  grothpw  9686  ordpipq  9802  ltbtwnnq  9838  mappsrpr  9967  map2psrpr  9969  elreal2  9991  le2tri3i  10205  elnn0nn  11373  elnnnn0b  11375  elnnnn0c  11376  elnnz  11425  elnn0z  11428  elz2  11432  elnnz1  11441  eluz2b2  11799  elnn1uz2  11803  elioo4g  12272  eluzfz2b  12388  fzn0  12393  elfz1end  12409  fzass4  12417  elfz1b  12447  nn0fz0  12476  fzolb  12515  fzon0  12526  elfzo0  12548  elfzo0z  12549  elfzo1  12557  fzo1fzo0n0  12558  om2uzrani  12791  nn0opthi  13097  hashkf  13159  isfinite4  13191  hashprb  13223  hashf1  13279  elss2prb  13307  iswrdb  13343  wrdexb  13348  0wrd0  13363  wrdl3s3  13751  cotr2g  13761  trclun  13799  sqr0lem  14025  rexanuz  14129  rexuz3  14132  fsum0diag  14553  fprod0diag  14761  divalgmod  15176  sadcp1  15224  isprm6  15473  nnoddn2prmb  15565  4sqlem4  15703  mreunirn  16308  isdrs2  16986  isacs5  17219  isacs4  17220  isacs3  17221  dfgrp2  17494  dfgrp3  17561  dfgrp3e  17562  isnsg3  17675  gicer  17765  oppgmndb  17831  oppggrpb  17834  pmtrfb  17931  invghm  18285  opprringb  18678  isnzr2hash  19312  abvn0b  19350  gzrngunit  19860  dvdsrzring  19879  zringunit  19884  zlmlmod  19919  zlmassa  19920  cygth  19968  frgpcyg  19970  toprntopon  20777  tgclb  20822  iscldtop  20947  isnrm2  21210  isnrm3  21211  discmp  21249  dfconn2  21270  2ndcsb  21300  dis2ndc  21311  loclly  21338  unisngl  21378  locfindis  21381  iskgen2  21399  dfac14  21469  kqtop  21596  kqt0  21597  kqreg  21602  kqnrm  21603  hmpher  21635  hmphsymb  21637  hmph0  21646  kqhmph  21670  ist1-5lem  21671  elmptrab2  21679  isfil2  21707  filunirn  21733  isufil2  21759  hausflim  21832  isfcls  21860  alexsubALT  21902  istgp2  21942  ustbas  22078  xmetunirn  22189  dscmet  22424  dscopn  22425  isngp4  22463  zcld  22663  zlmclm  22958  iscmet2  23138  iundisj  23362  i1f1lem  23501  fta1b  23974  elply2  23997  elqaa  24122  aannenlem2  24129  wilth  24842  lgsne0  25105  2lgs  25177  2sqlem2  25188  ostth  25373  mptelee  25820  wrdupgr  26025  wrdumgr  26037  umgrislfupgr  26063  uspgrupgrushgr  26117  usgrumgruspgr  26120  usgruspgrb  26121  usgrislfuspgr  26124  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  wwlksnwwlksnon  26878  elwwlks2ons3  26920  clwwlknclwwlkdifsOLD  26947  clwwlkn1loopb  27006  eclclwwlkn1  27039  upgriseupth  27185  numclwwlkovh  27353  nmlno0lem  27776  isblo3i  27784  blocni  27788  hvsubeq0i  28048  hvaddcani  28050  bcseqi  28105  isch3  28226  norm1exi  28235  hhsssh  28254  shslubi  28372  dfch2  28394  pjoc1i  28418  pjchi  28419  shs00i  28437  chsscon3i  28448  chlejb1i  28463  chj00i  28474  shjshseli  28480  h1de2ctlem  28542  spanunsni  28566  cmcmi  28579  cmbr3i  28587  cmbr4i  28588  pj11i  28698  hosubeq0i  28813  dmadjrnb  28893  nmlnop0iALT  28982  lnopeq0i  28994  elunop2  29000  lnconi  29020  lncnopbd  29024  adjbdlnb  29071  adjbd1o  29072  adjeq0  29078  rnbra  29094  pjss1coi  29150  pjss2coi  29151  pjnormssi  29155  pjssdif2i  29161  pjssdif1i  29162  dfpjop  29169  pjinvari  29178  pjin2i  29180  pjci  29187  pjcmul1i  29188  pjcmul2i  29189  strb  29245  hstrbi  29253  mdsl1i  29308  atom1d  29340  chrelat2i  29352  cvbr4i  29354  cvexchi  29356  sumdmdi  29407  dmdbr4ati  29408  dmdbr5ati  29409  dmdbr6ati  29410  dmdbr7ati  29411  cdj3i  29428  difeq  29481  iundisjf  29528  cnvoprabOLD  29626  fpwrelmap  29636  iundisjfi  29683  xrge0tsmsbi  29914  issgon  30314  measbasedom  30393  oddpwdc  30544  eulerpartlemt  30561  ballotlem2  30678  ballotlemrinv  30723  bnj1533  31048  bnj983  31147  elmsta  31571  nepss  31725  dford5  31734  dfpo2  31771  dfon2  31821  distel  31833  elno2  31932  bdayfo  31953  fnimage  32161  altopthsn  32193  ellines  32384  rankeq1o  32403  opnrebl2  32441  df3nandALT1  32521  pm4.81ALT  32671  bj-dfbi6  32685  bj-consensus  32687  bj-falor2  32695  bj-bibibi  32696  bj-andnotim  32698  bj-ssbeq  32752  bj-ssb0  32753  bj-19.41al  32762  bj-sb56  32764  bj-eqs  32788  bj-cbvexw  32789  bj-sb  32802  bj-equs45fv  32877  bj-sbfvv  32890  bj-sb6  32892  bj-axext4  32895  bj-hbaeb2  32930  bj-hbnaeb  32932  bj-equsal  32938  bj-sbsb  32949  bj-mo3OLD  32957  bj-cleqhyp  33017  bj-csbsnlem  33023  bj-snsetex  33076  bj-snglex  33086  bj-1uplth  33120  bj-1uplex  33121  bj-2uplth  33134  bj-2uplex  33135  bj-restpw  33170  bj-restuni  33175  bj-ismooredr2  33190  bj-discrmoore  33191  bj-snmoore  33193  bj-elid  33215  bj-elid3  33217  bj-eldiag2  33222  mptsnunlem  33315  topdifinf  33327  elxp8  33349  finxp1o  33359  wl-nfnbi  33444  wl-exeq  33451  wl-aleq  33452  wl-nfeqfb  33453  wl-ax11-lem6  33497  volsupnfl  33584  cover2  33638  isbnd3  33713  cntotbnd  33725  heibor  33750  isfld2  33934  isfldidl  33997  orfa  34011  eqelb  34145  iss2  34252  issetssr  34393  prtlem16  34473  isltrn2N  35724  ismrc  37581  isnacs3  37590  rexzrexnn0  37685  eldioph4b  37692  dford3  37912  wopprc  37914  ttac  37920  pw2f1ocnv  37921  dfac11  37949  dfac21  37953  isnumbasabl  37993  isnumbasgrp  37994  dfacbasgrp  37995  aaitgo  38049  ifpbi1b  38165  rp-fakeimass  38174  rp-fakeanorass  38175  rp-fakenanass  38177  rp-isfinite5  38180  rp-isfinite6  38181  rtrclex  38241  cnvtrrel  38279  rp-imass  38382  frege54cor0a  38474  isotone1  38663  isotone2  38664  gneispace  38749  k0004lem3  38764  nanorxor  38821  nzss  38833  pm10.55  38885  pm11.57  38906  sbeqalbi  38918  pm13.192  38928  pm13.194  38930  ipo0  38970  ifr0  38971  xpexb  38975  3impexpbicom  39002  com3rgbi  39037  pm2.43bgbi  39040  pm2.43cbi  39041  sb5ALT  39048  trsbc  39067  2pm13.193  39085  ax6e2ndeq  39092  2uasbanh  39094  eelT01  39253  eel0T1  39254  uunT1  39324  zfregs2VD  39390  equncomVD  39418  trsbcVD  39427  undif3VD  39432  2pm13.193VD  39453  ax6e2eqVD  39457  ax6e2ndeqVD  39459  2uasbanhVD  39461  ax6e2ndeqALT  39481  fompt  39693  mptssid  39764  elfzfzo  39802  allbutfi  39929  uzn0bi  40002  dvnprodlem3  40481  elaa2  40769  sge00  40911  ismea  40986  elhoi  41077  ovn0  41101  ovolval4lem2  41185  confun  41427  reuan  41501  afvfv0bi  41553  ffnafv  41572  sbgoldbmb  41999  mgm2mgm  42188  isringrng  42206  nnpw2pb  42706  elsetrecs  42771  elpg  42785
  Copyright terms: Public domain W3C validator