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  584  pm4.44  600  pm4.79  606  anass  680  jaob  821  jcab  906  andi  910  pm4.72  919  oibabs  924  pm4.82  968  cases2  992  consensus  998  3impexp  1286  3jaob  1387  tbw-bijust  1620  tbw-negdf  1621  19.26  1797  19.35  1805  19.21v  1870  sbbii  1889  19.9v  1898  19.23v  1904  19.41v  1916  equcom  1947  equvinv  1961  equvinvOLD  1964  equvelv  1965  cbvalw  1970  alcom  2039  19.3  2072  19.41  2106  cbvalv1  2179  19.3OLD  2206  cbval  2275  cbvalv  2277  equsex  2297  aecom  2315  equs45f  2354  dfsb2  2377  sb6f  2389  sbim  2399  sb6  2433  mo2v  2481  exmoeu  2506  mo3  2511  moanim  2533  euan  2534  2mo  2555  2eu6  2562  axext4  2610  eqcom  2633  nebi  2876  r19.26  3062  ralcom3  3100  ceqsex  3232  gencbvex  3241  gencbvex2  3242  eqvinc  3318  clel5  3331  pm13.183  3332  rr19.3v  3333  rr19.28v  3334  euxfr2  3378  reu6  3382  reu3  3383  sspss  3689  complss  3734  unineq  3858  uneqin  3859  undif3OLD  3870  difrab  3882  sbnfc2  3984  un00  3988  ssdifeq0  4028  r19.2zb  4038  ralf0OLD  4056  elpr2OLD  4176  snidb  4183  rabsnifsb  4232  tppreqb  4310  difsnb  4311  pwpw0  4317  sssn  4331  preq12b  4355  preqsnOLD  4367  pwsnALT  4402  unissint  4471  uniintsn  4484  iununi  4581  intex  4785  intnex  4786  iin0  4804  axpweq  4807  eusvnfb  4827  eusv2nf  4829  ralxfrALT  4852  nfcvb  4863  sspwb  4883  unipw  4884  opnz  4907  opth  4910  propeqop  4935  opthwiener  4941  ssopab2b  4967  pwssun  4985  opelxp  5111  opthprc  5132  relop  5237  issetid  5241  xpid11  5311  elres  5398  eldmeldmressn  5403  iss  5410  restidsingOLD  5422  issref  5472  asymref2  5476  xpnz  5516  xpdifid  5525  ssrnres  5535  dfrel2  5546  relrelss  5621  unixp0  5631  fn0  5970  funssxp  6020  f00  6046  f0bi  6047  dffo2  6078  f1o00  6130  fo00  6131  fv3  6164  dffn5  6199  dff2  6328  dff3  6329  dffo4  6332  dffo5  6333  exfo  6334  fmpt  6338  ffnfv  6344  fsn  6357  fsn2  6358  funop  6369  funsneqopb  6374  fnsnb  6387  isores1  6539  ssoprab2b  6666  eqfnov2  6721  unexb  6912  uniexb  6922  iunpw  6926  ordeleqon  6936  onintrab  6949  unon  6979  onuninsuci  6988  ordzsl  6993  onzsl  6994  f1oexbi  7066  ffoss  7077  1st2ndb  7154  suppssov1  7273  suppssfv  7277  reldmtpos  7306  dfrecs3  7415  omopthi  7683  ecopover  7797  mapsn  7844  mapsncnv  7849  mptelixpg  7890  elixpsn  7892  ixpsnf1o  7893  bren2  7931  en0  7964  en1  7968  en1b  7969  sbthb  8026  canth2  8058  onfin2  8097  sdom1  8105  1sdom  8108  fineqv  8120  unfilem1  8169  fiint  8182  residfi  8192  pwfi  8206  unifpw  8214  wofib  8395  sucprcreg  8451  opthreg  8460  suc11reg  8461  infeq5  8479  rankwflemb  8601  r1elss  8614  pwwf  8615  unwf  8618  uniwf  8627  rankonid  8637  rankr1id  8670  rankuni  8671  rankxplim3  8689  scott0  8694  karden  8703  isnum3  8725  oncard  8731  card1  8739  cardlim  8743  cardmin2  8769  pm54.43lem  8770  ween  8803  acnnum  8820  alephsuc2  8848  alephgeom  8850  iscard3  8861  dfac3  8889  dfac4  8890  dfac5lem3  8893  dfac5  8896  dfac2  8898  dfac8  8902  dfac9  8903  dfacacn  8908  dfac13  8909  dfac12r  8913  dfac12k  8914  kmlem2  8918  kmlem13  8929  cdainf  8959  ackbij2  9010  cflim2  9030  isfin4-2  9081  isfin4-3  9082  isf33lem  9133  compsscnv  9138  fin1a2lem6  9172  domtriom  9210  ac9  9250  ac9s  9260  fodomb  9293  brdom3  9295  brdom5  9296  brdom4  9297  brdom7disj  9298  brdom6disj  9299  iunfo  9306  sdomsdomcard  9327  gch2  9442  gch3  9443  eltsk2g  9518  grutsk  9589  grothpw  9593  ordpipq  9709  ltbtwnnq  9745  mappsrpr  9874  map2psrpr  9876  elreal2  9898  le2tri3i  10112  elnn0nn  11280  elnnnn0b  11282  elnnnn0c  11283  elnnz  11332  elnn0z  11335  elz2  11339  elnnz1  11348  eluz2b2  11705  elnn1uz2  11709  elioo4g  12173  eluzfz2b  12289  fzn0  12294  elfz1end  12310  fzass4  12318  elfz1b  12348  nn0fz0  12375  fzolb  12414  fzon0  12425  elfzo0  12446  elfzo0z  12447  elfzo1  12455  fzo1fzo0n0  12456  om2uzrani  12688  nn0opthi  12994  hashkf  13056  isfinite4  13090  hashprb  13122  hashf1  13176  elss2prb  13202  iswrdb  13245  wrdexb  13250  0wrd0  13265  wrdl3s3  13634  cotr2g  13644  trclun  13684  sqr0lem  13910  rexanuz  14014  rexuz3  14017  fsum0diag  14432  fprod0diag  14637  divalgmod  15048  sadcp1  15096  isprm6  15345  nnoddn2prmb  15437  4sqlem4  15575  mreunirn  16177  isdrs2  16855  isacs5  17088  isacs4  17089  isacs3  17090  dfgrp2  17363  dfgrp3  17430  dfgrp3e  17431  isnsg3  17544  gicer  17634  gicerOLD  17635  oppgmndb  17701  oppggrpb  17704  pmtrfb  17801  invghm  18155  opprringb  18548  isnzr2hash  19178  abvn0b  19216  gzrngunit  19726  dvdsrzring  19745  zringunit  19750  zlmlmod  19785  zlmassa  19786  cygth  19834  frgpcyg  19836  tgclb  20680  iscldtop  20804  isnrm2  21067  isnrm3  21068  discmp  21106  dfconn2  21127  2ndcsb  21157  dis2ndc  21168  loclly  21195  unisngl  21235  locfindis  21238  iskgen2  21256  dfac14  21326  kqtop  21453  kqt0  21454  kqreg  21459  kqnrm  21460  hmpher  21492  hmphsymb  21494  hmph0  21503  kqhmph  21527  ist1-5lem  21528  elmptrab2OLD  21536  elmptrab2  21537  isfil2  21565  filunirn  21591  isufil2  21617  hausflim  21690  isfcls  21718  alexsubALT  21760  istgp2  21800  ustbas  21936  xmetunirn  22047  dscmet  22282  dscopn  22283  isngp4  22321  zcld  22519  zlmclm  22815  iscmet2  22995  iundisj  23218  i1f1lem  23357  fta1b  23828  elply2  23851  elqaa  23976  aannenlem2  23983  wilth  24692  lgsne0  24955  2lgs  25027  2sqlem2  25038  ostth  25223  mptelee  25670  wrdupgr  25871  wrdumgr  25882  umgrislfupgr  25908  uspgrupgrushgr  25959  usgrumgruspgr  25962  usgruspgrb  25963  usgrislfuspgr  25966  uvtxa01vtx0  26178  clwwlknclwwlkdifs  26734  eclclwwlksn1  26812  upgriseupth  26927  nmlno0lem  27488  isblo3i  27496  blocni  27500  hvsubeq0i  27760  hvaddcani  27762  bcseqi  27817  isch3  27938  norm1exi  27947  hhsssh  27966  shslubi  28084  dfch2  28106  pjoc1i  28130  pjchi  28131  shs00i  28149  chsscon3i  28160  chlejb1i  28175  chj00i  28186  shjshseli  28192  h1de2ctlem  28254  spanunsni  28278  cmcmi  28291  cmbr3i  28299  cmbr4i  28300  pj11i  28410  hosubeq0i  28525  dmadjrnb  28605  nmlnop0iALT  28694  lnopeq0i  28706  elunop2  28712  lnconi  28732  lncnopbd  28736  adjbdlnb  28783  adjbd1o  28784  adjeq0  28790  rnbra  28806  pjss1coi  28862  pjss2coi  28863  pjnormssi  28867  pjssdif2i  28873  pjssdif1i  28874  dfpjop  28881  pjinvari  28890  pjin2i  28892  pjci  28899  pjcmul1i  28900  pjcmul2i  28901  strb  28957  hstrbi  28965  mdsl1i  29020  atom1d  29052  chrelat2i  29064  cvbr4i  29066  cvexchi  29068  sumdmdi  29119  dmdbr4ati  29120  dmdbr5ati  29121  dmdbr6ati  29122  dmdbr7ati  29123  cdj3i  29140  difeq  29193  iundisjf  29238  cnvoprab  29332  fpwrelmap  29342  iundisjfi  29388  xrge0tsmsbi  29563  issgon  29959  measbasedom  30038  oddpwdc  30189  eulerpartlemt  30206  ballotlem2  30323  ballotlemrinv  30368  bnj1533  30622  bnj983  30721  elmsta  31145  nepss  31300  dfpo2  31344  dfon2  31386  distel  31398  elno2  31496  bdayfo  31519  fnimage  31651  altopthsn  31683  ellines  31874  rankeq1o  31893  opnrebl2  31931  df3nandALT1  32011  pm4.81ALT  32161  bj-dfbi6  32175  bj-consensus  32177  bj-falor2  32185  bj-bibibi  32186  bj-andnotim  32188  bj-ssbeq  32242  bj-ssb0  32243  bj-19.41al  32252  bj-sb56  32254  bj-eqs  32278  bj-cbvexw  32279  bj-sb  32292  bj-equs45fv  32368  bj-sbfvv  32381  bj-sb6  32383  bj-axext4  32386  bj-hbaeb2  32421  bj-hbnaeb  32423  bj-equsal  32429  bj-sbsb  32440  bj-mo3OLD  32450  bj-cleqhyp  32512  bj-csbsnlem  32518  bj-snsetex  32571  bj-snglex  32581  bj-1uplth  32615  bj-1uplex  32616  bj-2uplth  32629  bj-2uplex  32630  bj-restpw  32655  bj-restuni  32660  bj-elpw3  32666  bj-toprntopon  32673  bj-elid  32691  bj-elid3  32693  bj-eldiag2  32698  mptsnunlem  32790  topdifinf  32802  elxp8  32824  finxp1o  32834  wl-nfnbi  32922  wl-exeq  32929  wl-aleq  32930  wl-nfeqfb  32931  wl-ax11-lem6  32975  volsupnfl  33053  cover2  33107  isbnd3  33182  cntotbnd  33194  heibor  33219  isfld2  33403  isfldidl  33466  orfa  33480  prtlem16  33601  isltrn2N  34853  ismrc  36711  isnacs3  36720  rexzrexnn0  36815  eldioph4b  36822  dford3  37042  wopprc  37044  ttac  37050  pw2f1ocnv  37051  dfac11  37079  dfac21  37083  isnumbasabl  37124  isnumbasgrp  37125  dfacbasgrp  37126  aaitgo  37180  ifpbi1b  37296  rp-fakeimass  37305  rp-fakeanorass  37306  rp-fakenanass  37308  rp-isfinite5  37311  rp-isfinite6  37312  rtrclex  37372  cnvtrrel  37410  rp-imass  37514  frege54cor0a  37606  isotone1  37795  isotone2  37796  gneispace  37881  k0004lem3  37896  nanorxor  37953  nzss  37965  pm10.55  38017  pm11.57  38038  sbeqalbi  38050  pm13.192  38060  pm13.194  38062  ipo0  38102  ifr0  38103  xpexb  38107  3impexpbicom  38134  com3rgbi  38169  pm2.43bgbi  38172  pm2.43cbi  38173  sb5ALT  38180  trsbc  38199  2pm13.193  38217  ax6e2ndeq  38224  2uasbanh  38226  eelT01  38385  eel0T1  38386  uunT1  38456  zfregs2VD  38526  equncomVD  38554  trsbcVD  38563  undif3VD  38568  2pm13.193VD  38589  ax6e2eqVD  38593  ax6e2ndeqVD  38595  2uasbanhVD  38597  ax6e2ndeqALT  38617  fompt  38820  mptssid  38893  elfzfzo  38920  allbutfi  39048  dvnprodlem3  39437  elaa2  39726  sge00  39868  ismea  39943  elhoi  40031  ovn0  40055  ovolval4lem2  40139  confun  40378  reuan  40452  afvfv0bi  40504  ffnafv  40523  mgm2mgm  41105  isringrng  41123  nnpw2pb  41628  ssdifsn  41677  elsetrecs  41693  elpg  41705
  Copyright terms: Public domain W3C validator