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

Theorem impbii 198
Description: Infer an equivalence from an implication and its converse. Inference associated with impbi 197. (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 197 . 2 ((𝜑𝜓) → ((𝜓𝜑) → (𝜑𝜓)))
41, 2, 3mp2 9 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  dfbi1  202  bicom  211  biid  250  2th  253  pm5.74  258  bitri  263  notnotb  303  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  583  pm4.44  599  pm4.79  605  anass  679  jaob  818  jcab  903  andi  907  pm4.72  916  oibabs  921  pm4.82  965  consensus  990  cases2  1005  3impexp  1281  3jaob  1382  tbw-bijust  1614  tbw-negdf  1615  19.26  1786  19.35  1794  19.21v  1855  sbbii  1874  19.9v  1883  19.23v  1889  19.41v  1901  equcom  1932  equvinv  1946  equvinvOLD  1949  equvelv  1950  cbvalw  1955  alcom  2024  19.3  2057  19.41  2090  cbvalv1  2163  19.3OLD  2190  cbval  2259  cbvalv  2261  equsex  2281  aecom  2299  equs45f  2338  dfsb2  2361  sb6f  2373  sbim  2383  sb6  2417  mo2v  2465  exmoeu  2490  mo3  2495  moanim  2517  euan  2518  2mo  2539  2eu6  2546  axext4  2594  eqcom  2617  nebi  2862  r19.26  3046  ralcom3  3084  ceqsex  3214  gencbvex  3223  gencbvex2  3224  eqvinc  3300  pm13.183  3313  rr19.3v  3314  rr19.28v  3315  euxfr2  3358  reu6  3362  reu3  3363  sspss  3668  complss  3713  unineq  3836  uneqin  3837  undif3OLD  3848  difrab  3860  sbnfc2  3959  un00  3963  ssdifeq0  4003  r19.2zb  4013  ralf0OLD  4031  elpr2OLD  4148  snidb  4154  rabsnifsb  4201  tppreqb  4277  difsnb  4278  pwpw0  4284  sssn  4298  preq12b  4322  preqsnOLD  4332  pwsnALT  4367  unissint  4436  uniintsn  4449  iununi  4546  intex  4747  intnex  4748  iin0  4765  axpweq  4768  eusvnfb  4788  eusv2nf  4790  ralxfrALT  4813  nfcvb  4824  sspwb  4844  unipw  4845  opnz  4868  opth  4871  propeqop  4895  opthwiener  4901  ssopab2b  4927  pwssun  4944  opelxp  5070  opthprc  5089  relop  5194  issetid  5198  xpid11  5268  elres  5355  eldmeldmressn  5360  iss  5367  restidsingOLD  5378  issref  5428  asymref2  5432  xpnz  5472  xpdifid  5481  ssrnres  5491  dfrel2  5502  relrelss  5576  unixp0  5586  fn0  5924  funssxp  5974  f00  6000  f0bi  6001  dffo2  6032  f1o00  6083  fo00  6084  fv3  6116  dffn5  6151  dff2  6279  dff3  6280  dffo4  6283  dffo5  6284  exfo  6285  fmpt  6289  ffnfv  6295  fsn  6308  fsn2  6309  funop  6320  funsneqopb  6324  fnsnb  6337  isores1  6484  ssoprab2b  6610  eqfnov2  6665  unexb  6856  uniexb  6866  iunpw  6870  ordeleqon  6880  onintrab  6893  unon  6923  onuninsuci  6932  ordzsl  6937  onzsl  6938  f1oexbi  7009  ffoss  7020  1st2ndb  7097  suppssov1  7214  suppssfv  7218  reldmtpos  7247  dfrecs3  7356  omopthi  7624  ecopover  7738  mapsn  7785  mapsncnv  7790  mptelixpg  7831  elixpsn  7833  ixpsnf1o  7834  bren2  7872  en0  7905  en1  7909  en1b  7910  sbthb  7966  canth2  7998  onfin2  8037  sdom1  8045  1sdom  8048  fineqv  8060  unfilem1  8109  fiint  8122  pwfi  8144  unifpw  8152  wofib  8333  sucprcreg  8389  opthreg  8398  suc11reg  8399  infeq5  8417  rankwflemb  8539  r1elss  8552  pwwf  8553  unwf  8556  uniwf  8565  rankonid  8575  rankr1id  8608  rankuni  8609  rankxplim3  8627  scott0  8632  karden  8641  isnum3  8663  oncard  8669  card1  8677  cardlim  8681  cardmin2  8707  pm54.43lem  8708  ween  8741  acnnum  8758  alephsuc2  8786  alephgeom  8788  iscard3  8799  dfac3  8827  dfac4  8828  dfac5lem3  8831  dfac5  8834  dfac2  8836  dfac8  8840  dfac9  8841  dfacacn  8846  dfac13  8847  dfac12r  8851  dfac12k  8852  kmlem2  8856  kmlem13  8867  cdainf  8897  ackbij2  8948  cflim2  8968  isfin4-2  9019  isfin4-3  9020  isf33lem  9071  compsscnv  9076  fin1a2lem6  9110  domtriom  9148  ac9  9188  ac9s  9198  fodomb  9229  brdom3  9231  brdom5  9232  brdom4  9233  brdom7disj  9234  brdom6disj  9235  iunfo  9240  sdomsdomcard  9261  gch2  9376  gch3  9377  eltsk2g  9452  grutsk  9523  grothpw  9527  ordpipq  9643  ltbtwnnq  9679  mappsrpr  9808  map2psrpr  9810  elreal2  9832  le2tri3i  10046  elnn0nn  11212  elnnnn0b  11214  elnnnn0c  11215  elnnz  11264  elnn0z  11267  elz2  11271  elnnz1  11280  eluz2b2  11637  elnn1uz2  11641  elioo4g  12105  eluzfz2b  12221  fzn0  12226  elfz1end  12242  fzass4  12250  elfz1b  12279  nn0fz0  12306  fzolb  12345  fzon0  12356  elfzo0  12376  elfzo0z  12377  elfzo1  12385  fzo1fzo0n0  12386  om2uzrani  12613  nn0opthi  12919  hashkf  12981  isfinite4  13014  hashprb  13046  hashf1  13098  elss2prb  13123  iswrdb  13166  wrdexb  13171  0wrd0  13186  wrdl3s3  13553  cotr2g  13563  trclun  13603  sqr0lem  13829  rexanuz  13933  rexuz3  13936  fsum0diag  14351  fprod0diag  14556  divalgmod  14967  sadcp1  15015  isprm6  15264  nnoddn2prmb  15356  4sqlem4  15494  mreunirn  16084  isdrs2  16762  isacs5  16995  isacs4  16996  isacs3  16997  dfgrp2  17270  dfgrp3  17337  dfgrp3e  17338  isnsg3  17451  gicer  17541  gicerOLD  17542  oppgmndb  17608  oppggrpb  17611  pmtrfb  17708  invghm  18062  opprringb  18455  isnzr2hash  19085  abvn0b  19123  gzrngunit  19631  dvdsrzring  19650  zringunit  19655  zlmlmod  19690  zlmassa  19691  cygth  19739  frgpcyg  19741  tgclb  20585  iscldtop  20709  isnrm2  20972  isnrm3  20973  discmp  21011  dfcon2  21032  2ndcsb  21062  dis2ndc  21073  loclly  21100  unisngl  21140  locfindis  21143  iskgen2  21161  dfac14  21231  kqtop  21358  kqt0  21359  kqreg  21364  kqnrm  21365  hmpher  21397  hmphsymb  21399  hmph0  21408  kqhmph  21432  ist1-5lem  21433  elmptrab2OLD  21441  elmptrab2  21442  isfil2  21470  filunirn  21496  isufil2  21522  hausflim  21595  isfcls  21623  alexsubALT  21665  istgp2  21705  ustbas  21841  xmetunirn  21952  dscmet  22187  dscopn  22188  isngp4  22226  zcld  22424  zlmclm  22720  iscmet2  22900  iundisj  23123  i1f1lem  23262  fta1b  23733  elply2  23756  elqaa  23881  aannenlem2  23888  wilth  24597  lgsne0  24860  2lgs  24932  2sqlem2  24943  ostth  25128  mptelee  25575  wrdupgr  25752  wrdumgr  25763  umgrislfupgr  25789  uhgra0v  25839  wrdumgra  25845  usgra0v  25900  uvtx01vtx  26020  wlkcpr  26057  isspthonpth  26114  eclclwwlkn1  26359  usg2spthonot1  26417  clwlknclwlkdifs  26487  frgra0v  26520  nmlno0lem  27032  isblo3i  27040  blocni  27044  hvsubeq0i  27304  hvaddcani  27306  bcseqi  27361  isch3  27482  norm1exi  27491  hhsssh  27510  shslubi  27628  dfch2  27650  pjoc1i  27674  pjchi  27675  shs00i  27693  chsscon3i  27704  chlejb1i  27719  chj00i  27730  shjshseli  27736  h1de2ctlem  27798  spanunsni  27822  cmcmi  27835  cmbr3i  27843  cmbr4i  27844  pj11i  27954  hosubeq0i  28069  dmadjrnb  28149  nmlnop0iALT  28238  lnopeq0i  28250  elunop2  28256  lnconi  28276  lncnopbd  28280  adjbdlnb  28327  adjbd1o  28328  adjeq0  28334  rnbra  28350  pjss1coi  28406  pjss2coi  28407  pjnormssi  28411  pjssdif2i  28417  pjssdif1i  28418  dfpjop  28425  pjinvari  28434  pjin2i  28436  pjci  28443  pjcmul1i  28444  pjcmul2i  28445  strb  28501  hstrbi  28509  mdsl1i  28564  atom1d  28596  chrelat2i  28608  cvbr4i  28610  cvexchi  28612  sumdmdi  28663  dmdbr4ati  28664  dmdbr5ati  28665  dmdbr6ati  28666  dmdbr7ati  28667  cdj3i  28684  difeq  28739  iundisjf  28784  cnvoprab  28886  fpwrelmap  28896  iundisjfi  28942  xrge0tsmsbi  29117  issgon  29513  measbasedom  29592  oddpwdc  29743  eulerpartlemt  29760  ballotlem2  29877  ballotlemrinv  29922  bnj1533  30176  bnj983  30275  elmsta  30699  nepss  30854  dfpo2  30898  dfon2  30941  distel  30953  elno2  31051  bdayfo  31074  fnimage  31206  altopthsn  31238  ellines  31429  rankeq1o  31448  opnrebl2  31486  df3nandALT1  31566  pm4.81ALT  31716  bj-dfbi6  31730  bj-consensus  31732  bj-falor2  31743  bj-bibibi  31744  bj-andnotim  31746  bj-ssbeq  31816  bj-ssb0  31817  bj-19.41al  31826  bj-sb56  31828  bj-eqs  31850  bj-cbvexw  31851  bj-sb  31864  bj-equs45fv  31940  bj-sbfvv  31953  bj-sb6  31955  bj-axext4  31958  bj-hbaeb2  31993  bj-hbnaeb  31995  bj-equsal  32001  bj-sbsb  32012  bj-mo3OLD  32022  bj-cleqhyp  32084  bj-csbsnlem  32090  bj-snsetex  32144  bj-snglex  32154  bj-1uplth  32188  bj-1uplex  32189  bj-2uplth  32202  bj-2uplex  32203  bj-restpw  32226  bj-restuni  32231  bj-elpw3  32237  bj-toprntopon  32244  bj-elid  32262  bj-elid3  32264  bj-eldiag2  32269  mptsnunlem  32361  topdifinf  32373  elxp8  32395  finxp1o  32405  wl-nfnbi  32493  wl-exeq  32500  wl-aleq  32501  wl-nfeqfb  32502  wl-ax11-lem6  32546  volsupnfl  32624  cover2  32678  isbnd3  32753  cntotbnd  32765  heibor  32790  isfld2  32974  isfldidl  33037  orfa  33051  prtlem16  33172  isltrn2N  34424  ismrc  36282  isnacs3  36291  rexzrexnn0  36386  eldioph4b  36393  dford3  36613  wopprc  36615  ttac  36621  pw2f1ocnv  36622  dfac11  36650  dfac21  36654  isnumbasabl  36695  isnumbasgrp  36696  dfacbasgrp  36697  aaitgo  36751  ifpbi1b  36867  rp-fakeimass  36876  rp-fakeanorass  36877  rp-fakenanass  36879  rp-isfinite5  36882  rp-isfinite6  36883  rtrclex  36943  cnvtrrel  36981  rp-imass  37085  frege54cor0a  37177  isotone1  37366  isotone2  37367  gneispace  37452  k0004lem3  37467  nanorxor  37526  nzss  37538  pm10.55  37590  pm11.57  37611  sbeqalbi  37623  pm13.192  37633  pm13.194  37635  ipo0  37674  ifr0  37675  xpexb  37679  3impexpbicom  37706  com3rgbi  37741  pm2.43bgbi  37744  pm2.43cbi  37745  sb5ALT  37752  trsbc  37771  2pm13.193  37789  ax6e2ndeq  37796  2uasbanh  37798  eelT01  37957  eel0T1  37958  uunT1  38028  zfregs2VD  38098  equncomVD  38126  trsbcVD  38135  undif3VD  38140  2pm13.193VD  38161  ax6e2eqVD  38165  ax6e2ndeqVD  38167  2uasbanhVD  38169  ax6e2ndeqALT  38189  fompt  38374  elfzfzo  38429  allbutfi  38557  dvnprodlem3  38838  elaa2  39127  sge00  39269  ismea  39344  elhoi  39432  ovn0  39456  ovolval4lem2  39540  confun  39755  reuan  39829  afvfv0bi  39881  ffnafv  39900  clel5  40303  residfi  40340  uspgrupgrushgr  40407  usgrumgruspgr  40410  usgruspgrb  40411  usgrislfuspgr  40414  uvtxa01vtx0  40623  isclWlkb  40980  clwwlknclwwlkdifs  41181  eclclwwlksn1  41259  upgriseupth  41375  mgm2mgm  41653  isringrng  41671  nnpw2pb  42179  ssdifsn  42228  elsetrecs  42244  elpg  42256
  Copyright terms: Public domain W3C validator