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  1785  19.35  1793  19.21v  1854  sbbii  1873  19.9v  1882  19.23v  1888  19.41v  1900  equcom  1931  equvinv  1945  equvinvOLD  1948  equvelv  1949  cbvalw  1954  alcom  2023  19.3  2055  19.41  2088  cbvalv1  2161  19.3OLD  2188  cbval  2257  cbvalv  2259  equsex  2279  aecom  2298  equs45f  2337  dfsb2  2360  sb6f  2372  sbim  2382  sb6  2416  mo2v  2464  exmoeu  2489  mo3  2494  moanim  2516  euan  2517  2mo  2538  2eu6  2545  axext4  2593  eqcom  2616  nebi  2861  r19.26  3045  ralcom3  3083  ceqsex  3213  gencbvex  3222  gencbvex2  3223  eqvinc  3299  pm13.183  3312  rr19.3v  3313  rr19.28v  3314  euxfr2  3357  reu6  3361  reu3  3362  sspss  3667  complss  3712  unineq  3835  uneqin  3836  undif3OLD  3847  difrab  3859  sbnfc2  3958  un00  3962  ssdifeq0  4002  r19.2zb  4012  ralf0OLD  4030  elpr2OLD  4147  snidb  4153  rabsnifsb  4200  tppreqb  4276  difsnb  4277  pwpw0  4283  sssn  4295  preq12b  4317  preqsnOLD  4327  pwsnALT  4361  unissint  4430  uniintsn  4443  iununi  4540  intex  4742  intnex  4743  iin0  4760  axpweq  4763  eusvnfb  4783  eusv2nf  4785  ralxfrALT  4808  nfcvb  4819  sspwb  4838  unipw  4839  opnz  4862  opth  4865  opthwiener  4892  ssopab2b  4917  pwssun  4934  opelxp  5060  opthprc  5079  relop  5182  issetid  5186  xpid11  5255  elres  5342  eldmeldmressn  5347  iss  5354  restidsingOLD  5365  issref  5415  asymref2  5419  xpnz  5458  xpdifid  5467  ssrnres  5477  dfrel2  5488  relrelss  5562  unixp0  5572  fn0  5910  funssxp  5960  f00  5985  f0bi  5986  dffo2  6017  f1o00  6068  fo00  6069  fv3  6101  dffn5  6136  dff2  6264  dff3  6265  dffo4  6268  dffo5  6269  exfo  6270  fmpt  6274  ffnfv  6280  fsn  6293  fsn2  6294  fnsnb  6315  isores1  6462  ssoprab2b  6588  eqfnov2  6643  unexb  6833  uniexb  6843  iunpw  6847  ordeleqon  6857  onintrab  6870  unon  6900  onuninsuci  6909  ordzsl  6914  onzsl  6915  f1oexbi  6986  ffoss  6997  1st2ndb  7074  suppssov1  7191  suppssfv  7195  reldmtpos  7224  dfrecs3  7333  omopthi  7601  ecopover  7715  mapsn  7762  mapsncnv  7767  mptelixpg  7808  elixpsn  7810  ixpsnf1o  7811  bren2  7849  en0  7882  en1  7886  en1b  7887  sbthb  7943  canth2  7975  onfin2  8014  sdom1  8022  1sdom  8025  fineqv  8037  unfilem1  8086  fiint  8099  pwfi  8121  unifpw  8129  wofib  8310  sucprcreg  8366  opthreg  8375  suc11reg  8376  infeq5  8394  rankwflemb  8516  r1elss  8529  pwwf  8530  unwf  8533  uniwf  8542  rankonid  8552  rankr1id  8585  rankuni  8586  rankxplim3  8604  scott0  8609  karden  8618  isnum3  8640  oncard  8646  card1  8654  cardlim  8658  cardmin2  8684  pm54.43lem  8685  ween  8718  acnnum  8735  alephsuc2  8763  alephgeom  8765  iscard3  8776  dfac3  8804  dfac4  8805  dfac5lem3  8808  dfac5  8811  dfac2  8813  dfac8  8817  dfac9  8818  dfacacn  8823  dfac13  8824  dfac12r  8828  dfac12k  8829  kmlem2  8833  kmlem13  8844  cdainf  8874  ackbij2  8925  cflim2  8945  isfin4-2  8996  isfin4-3  8997  isf33lem  9048  compsscnv  9053  fin1a2lem6  9087  domtriom  9125  ac9  9165  ac9s  9175  fodomb  9206  brdom3  9208  brdom5  9209  brdom4  9210  brdom7disj  9211  brdom6disj  9212  iunfo  9217  sdomsdomcard  9238  gch2  9353  gch3  9354  eltsk2g  9429  grutsk  9500  grothpw  9504  ordpipq  9620  ltbtwnnq  9656  mappsrpr  9785  map2psrpr  9787  elreal2  9809  le2tri3i  10018  elnn0nn  11182  elnnnn0b  11184  elnnnn0c  11185  elnnz  11220  elnn0z  11223  elz2  11227  elnnz1  11236  eluz2b2  11593  elnn1uz2  11597  elioo4g  12061  eluzfz2b  12176  fzn0  12181  elfz1end  12197  fzass4  12205  elfz1b  12234  nn0fz0  12261  fzolb  12300  fzon0  12311  elfzo0  12331  elfzo0z  12332  elfzo1  12340  fzo1fzo0n0  12341  om2uzrani  12568  nn0opthi  12874  hashkf  12936  isfinite4  12966  hashprb  12998  hashf1  13050  elss2prb  13073  iswrdb  13112  wrdexb  13117  0wrd0  13132  wrdl3s3  13499  cotr2g  13509  trclun  13549  sqr0lem  13775  rexanuz  13879  rexuz3  13882  fsum0diag  14297  fprod0diag  14502  divalgmod  14913  sadcp1  14961  isprm6  15210  nnoddn2prmb  15302  4sqlem4  15440  mreunirn  16030  isdrs2  16708  isacs5  16941  isacs4  16942  isacs3  16943  dfgrp2  17216  dfgrp3  17283  dfgrp3e  17284  isnsg3  17397  gicer  17487  gicerOLD  17488  oppgmndb  17554  oppggrpb  17557  pmtrfb  17654  invghm  18008  opprringb  18401  isnzr2hash  19031  abvn0b  19069  gzrngunit  19577  dvdsrzring  19596  zringunit  19603  zlmlmod  19635  zlmassa  19636  cygth  19684  frgpcyg  19686  tgclb  20527  iscldtop  20651  isnrm2  20914  isnrm3  20915  discmp  20953  dfcon2  20974  2ndcsb  21004  dis2ndc  21015  loclly  21042  unisngl  21082  locfindis  21085  iskgen2  21103  dfac14  21173  kqtop  21300  kqt0  21301  kqreg  21306  kqnrm  21307  hmpher  21339  hmphsymb  21341  hmph0  21350  kqhmph  21374  ist1-5lem  21375  elmptrab2OLD  21383  elmptrab2  21384  isfil2  21412  filunirn  21438  isufil2  21464  hausflim  21537  isfcls  21565  alexsubALT  21607  istgp2  21647  ustbas  21783  xmetunirn  21893  dscmet  22128  dscopn  22129  isngp4  22166  zcld  22356  zlmclm  22651  iscmet2  22818  iundisj  23040  i1f1lem  23179  fta1b  23650  elply2  23673  elqaa  23798  aannenlem2  23805  wilth  24514  lgsne0  24777  2lgs  24849  2sqlem2  24860  ostth  25045  mptelee  25493  uhgra0v  25605  wrdumgra  25611  usgra0v  25666  uvtx01vtx  25786  wlkcpr  25823  isspthonpth  25880  eclclwwlkn1  26125  usg2spthonot1  26183  clwlknclwlkdifs  26253  frgra0v  26286  nmlno0lem  26838  isblo3i  26846  blocni  26850  hvsubeq0i  27110  hvaddcani  27112  bcseqi  27167  isch3  27288  norm1exi  27297  hhsssh  27316  shslubi  27434  dfch2  27456  pjoc1i  27480  pjchi  27481  shs00i  27499  chsscon3i  27510  chlejb1i  27525  chj00i  27536  shjshseli  27542  h1de2ctlem  27604  spanunsni  27628  cmcmi  27641  cmbr3i  27649  cmbr4i  27650  pj11i  27760  hosubeq0i  27875  dmadjrnb  27955  nmlnop0iALT  28044  lnopeq0i  28056  elunop2  28062  lnconi  28082  lncnopbd  28086  adjbdlnb  28133  adjbd1o  28134  adjeq0  28140  rnbra  28156  pjss1coi  28212  pjss2coi  28213  pjnormssi  28217  pjssdif2i  28223  pjssdif1i  28224  dfpjop  28231  pjinvari  28240  pjin2i  28242  pjci  28249  pjcmul1i  28250  pjcmul2i  28251  strb  28307  hstrbi  28315  mdsl1i  28370  atom1d  28402  chrelat2i  28414  cvbr4i  28416  cvexchi  28418  sumdmdi  28469  dmdbr4ati  28470  dmdbr5ati  28471  dmdbr6ati  28472  dmdbr7ati  28473  cdj3i  28490  difeq  28545  iundisjf  28590  cnvoprab  28692  fpwrelmap  28702  iundisjfi  28748  xrge0tsmsbi  28923  issgon  29319  measbasedom  29398  oddpwdc  29549  eulerpartlemt  29566  ballotlem2  29683  ballotlemrinv  29728  bnj1533  29982  bnj983  30081  elmsta  30505  nepss  30660  dfpo2  30704  dfon2  30747  distel  30759  elno2  30857  bdayfo  30880  fnimage  31012  altopthsn  31044  ellines  31235  rankeq1o  31254  opnrebl2  31292  df3nandALT1  31372  pm4.81ALT  31522  bj-dfbi6  31536  bj-consensus  31538  bj-falor2  31549  bj-bibibi  31550  bj-andnotim  31552  bj-ssbeq  31622  bj-ssb0  31623  bj-19.41al  31632  bj-sb56  31634  bj-eqs  31656  bj-cbvexw  31657  bj-sb  31670  bj-equs45fv  31748  bj-sbfvv  31763  bj-sb6  31766  bj-axext4  31771  bj-hbaeb2  31806  bj-hbnaeb  31808  bj-equsal  31814  bj-sbsb  31825  bj-mo3OLD  31835  bj-cleqhyp  31887  bj-csbsnlem  31893  bj-snsetex  31947  bj-snglex  31957  bj-1uplth  31991  bj-1uplex  31992  bj-2uplth  32005  bj-2uplex  32006  bj-restpw  32029  bj-restuni  32034  bj-elpw3  32040  bj-toprntopon  32047  bj-elid  32065  bj-elid3  32067  bj-eldiag2  32072  mptsnunlem  32164  topdifinf  32176  elxp8  32198  finxp1o  32208  wl-nfnbi  32296  wl-exeq  32303  wl-aleq  32304  wl-nfeqfb  32305  wl-ax11-lem6  32349  volsupnfl  32427  cover2  32481  isbnd3  32556  cntotbnd  32568  heibor  32593  isfld2  32777  isfldidl  32840  orfa  32854  prtlem16  32975  isltrn2N  34227  ismrc  36085  isnacs3  36094  rexzrexnn0  36189  eldioph4b  36196  dford3  36416  wopprc  36418  ttac  36424  pw2f1ocnv  36425  dfac11  36453  dfac21  36457  isnumbasabl  36498  isnumbasgrp  36499  dfacbasgrp  36500  aaitgo  36554  ifpbi1b  36670  rp-fakeimass  36679  rp-fakeanorass  36680  rp-fakenanass  36682  rp-isfinite5  36685  rp-isfinite6  36686  rtrclex  36746  cnvtrrel  36784  rp-imass  36888  frege54cor0a  36980  isotone1  37169  isotone2  37170  gneispace  37255  k0004lem3  37270  nanorxor  37329  nzss  37341  pm10.55  37393  pm11.57  37414  sbeqalbi  37426  pm13.192  37436  pm13.194  37438  ipo0  37477  ifr0  37478  xpexb  37482  3impexpbicom  37509  com3rgbi  37544  pm2.43bgbi  37547  pm2.43cbi  37548  sb5ALT  37555  trsbc  37574  2pm13.193  37592  ax6e2ndeq  37599  2uasbanh  37601  eelT01  37760  eel0T1  37761  uunT1  37831  zfregs2VD  37901  equncomVD  37929  trsbcVD  37938  undif3VD  37943  2pm13.193VD  37964  ax6e2eqVD  37968  ax6e2ndeqVD  37970  2uasbanhVD  37972  ax6e2ndeqALT  37992  fompt  38177  elfzfzo  38232  allbutfi  38361  dvnprodlem3  38642  elaa2  38931  sge00  39073  ismea  39148  elhoi  39236  ovn0  39260  ovolval4lem2  39344  confun  39559  reuan  39633  afvfv0bi  39686  ffnafv  39705  clel5  40108  propeqop  40126  funop  40145  funsneqopb  40151  residfi  40167  wrdupgr  40313  wrdumgr  40324  umgrislfupgr  40350  uspgrupgrushgr  40409  usgrumgruspgr  40412  usgruspgrb  40413  usgrislfuspgr  40416  uvtxa01vtx0  40625  isclWlkb  40982  clwwlknclwwlkdifs  41183  eclclwwlksn1  41261  upgriseupth  41377  mgm2mgm  41655  isringrng  41673  nnpw2pb  42181
  Copyright terms: Public domain W3C validator