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

Theorem impbii 212
Description: Infer an equivalence from an implication and its converse. Inference associated with impbi 211. (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 211 . 2 ((𝜑𝜓) → ((𝜓𝜑) → (𝜑𝜓)))
41, 2, 3mp2 9 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  bicom  225  biid  264  2th  267  pm5.74  273  bitri  278  notnotb  318  con34b  319  notbi  322  bibi2i  341  con1b  362  con2b  363  bi2.04  392  imdi  394  pm4.8  396  pm4.81  397  impexp  454  ancom  464  anass  472  jcab  521  impimprbi  827  orcom  867  dfor2  899  oridm  902  orbi2i  910  or12  918  biorfi  936  pm4.72  947  oibabs  949  jaob  959  pm4.44  994  pm4.79  1001  andi  1005  pm4.82  1021  cases2ALT  1044  consensus  1048  3impexp  1355  3jaob  1423  nanass  1501  norassOLD  1535  tbw-bijust  1700  tbw-negdf  1701  19.26  1871  19.35  1878  19.21v  1940  19.23v  1943  19.41v  1950  19.3v  1986  19.9v  1988  equcom  2025  cbvalw  2042  sbbii  2081  sban  2086  sbv  2098  alcom  2163  19.3  2203  19.41  2238  sb6OLD  2281  sbbibOLD  2290  sbim  2312  sbimvOLD  2326  cbvalv1  2362  cbval  2417  cbvalvOLD  2421  equsex  2441  aecom  2450  equs45f  2483  dfsb1  2511  dfsb2  2532  sb6f  2537  sbbiiALT  2578  sb6ALT  2585  dfsb2ALT  2591  sb6fALT  2602  sbimALT  2608  dfmoeu  2618  moabs  2625  mobii  2630  mo3  2647  mo4  2649  exmoeu  2665  moanimlem  2704  euan  2707  euanv  2710  2mo  2734  2eu6  2743  euae  2746  axextb  2797  eqcom  2829  nebi  3091  r19.26  3162  r19.35  3323  ralcom3  3345  ceqsex  3515  gencbvex  3524  gencbvex2  3525  pm13.183  3633  rr19.3v  3634  rr19.28v  3635  euxfr2w  3686  euxfr2  3688  reu6  3692  reu3  3693  reuan  3852  sspss  4051  complss  4098  unineq  4228  uneqin  4229  difrab  4251  sbnfc2  4360  un00  4366  ssdifeq0  4404  r19.2zb  4413  pwidb  4534  snidb  4574  rabsnifsb  4632  tppreqb  4711  difsnb  4712  pwpw0  4719  sssn  4732  preq12b  4754  pwsnOLD  4806  unissint  4875  uniintsn  4888  iununi  4996  al0ssb  5188  intex  5216  intnex  5217  iin0  5238  axpweq  5242  nfcvb  5254  eusvnfb  5271  eusv2nf  5273  ralxfrALT  5293  sspwb  5319  unipw  5320  opnz  5342  opth  5345  sbcop1  5356  opeqsng  5370  propeqop  5374  opthwiener  5381  opthhausdorff  5384  opthhausdorff0  5385  rexopabb  5392  ssopab2bw  5411  ssopab2b  5413  pwssun  5433  opelxp  5568  opthprc  5593  relsnb  5652  relop  5698  issetid  5702  xpid11  5779  elinxp  5868  eldmeldmressn  5874  iss  5881  iresn0n0  5901  asymref2  5955  xpnz  5994  xpdifid  6003  ssrnres  6013  dfrel2  6024  relrelss  6102  unixp0  6112  reuop  6122  fn0  6459  funssxp  6516  f00  6542  f0bi  6543  dffo2  6576  f1o00  6631  fo00  6632  fv3  6670  dffn5  6706  dff2  6847  dff3  6848  dffo4  6851  dffo5  6852  exfo  6853  fmpt  6856  ffnfv  6864  fsn  6879  fsn2  6880  funop  6893  funsneqopb  6896  fnsnb  6910  isores1  7071  ssoprab2b  7207  eqoprab2bw  7208  eqfnov2  7265  unexb  7456  uniexb  7471  pwexb  7473  iunpw  7478  ordeleqon  7488  onintrab  7501  unon  7531  onuninsuci  7540  ordzsl  7545  onzsl  7546  f1oexbi  7619  ffoss  7633  1st2ndb  7715  suppssov1  7849  suppssfv  7853  reldmtpos  7887  dfrecs3  7996  omopthi  8271  ecopover  8388  mapsncnv  8444  mptelixpg  8486  elixpsn  8488  ixpsnf1o  8489  bren2  8527  en0  8559  en1  8563  en1b  8564  sbthb  8626  canth2  8658  onfin2  8699  sdom1  8706  1sdom  8709  fineqv  8721  unfilem1  8770  fiint  8783  residfi  8793  pwfi  8807  unifpw  8815  wofib  8997  sucprcreg  9053  opthreg  9069  suc11reg  9070  infeq5  9088  rankwflemb  9210  r1elss  9223  pwwf  9224  unwf  9227  uniwf  9236  rankonid  9246  rankr1id  9279  rankuni  9280  rankxplim3  9298  scott0  9303  karden  9312  djuexb  9326  isnum3  9371  oncard  9377  card1  9385  cardlim  9389  cardmin2  9416  pm54.43lem  9417  ween  9450  acnnum  9467  alephsuc2  9495  alephgeom  9497  iscard3  9508  dfac3  9536  dfac4  9537  dfac5lem3  9540  dfac5  9543  dfac2  9546  dfac8  9550  dfac9  9551  dfacacn  9556  dfac13  9557  dfac12r  9561  dfac12k  9562  kmlem2  9566  kmlem13  9577  djuinf  9603  ackbij2  9654  cflim2  9674  isfin4-2  9725  isfin4p1  9726  isf33lem  9777  compsscnv  9782  fin1a2lem6  9816  domtriom  9854  ac9  9894  ac9s  9904  fodomb  9937  brdom3  9939  brdom5  9940  brdom4  9941  brdom7disj  9942  brdom6disj  9943  iunfo  9950  sdomsdomcard  9971  gch2  10086  gch3  10087  eltsk2g  10162  grutsk  10233  ordpipq  10353  ltbtwnnq  10389  mappsrpr  10519  map2psrpr  10521  elreal2  10543  le2tri3i  10759  elnn0nn  11927  elnnnn0b  11929  elnnnn0c  11930  elnnz  11979  elnn0z  11982  elz2  11987  elnnz1  11996  eluz2b2  12309  elnn1uz2  12313  elpqb  12363  elioo4g  12785  eluzfz2b  12911  fzn0  12916  elfz1end  12932  fzass4  12940  elfz1b  12971  nn0fz0  13000  fzolb  13039  fzon0  13050  elfzo0  13073  elfzo0z  13074  elfzo1  13082  fzo1fzo0n0  13083  om2uzrani  13315  nn0opthi  13626  hashkf  13688  isfinite4  13719  hashprb  13754  hashf1  13811  elss2prb  13841  iswrdb  13863  wrdexb  13868  0wrd0  13883  wrdl3s3  14317  cotr2g  14327  trclun  14365  sqr0lem  14591  rexanuz  14696  rexuz3  14699  fsum0diag  15123  fprod0diag  15331  divalgmod  15746  sadcp1  15793  isprm6  16047  nnoddn2prmb  16139  4sqlem4  16277  fnpr2ob  16822  mreunirn  16863  isdrs2  17540  isacs5  17773  isacs4  17774  isacs3  17775  dfgrp2  18119  dfgrp3  18189  dfgrp3e  18190  isnsg3  18303  gicer  18407  oppgmndb  18474  oppggrpb  18477  pmtrfb  18584  invghm  18945  opprringb  19376  isnzr2hash  20028  abvn0b  20066  gzrngunit  20155  dvdsrzring  20174  zringunit  20179  zlmlmod  20214  cygth  20261  frgpcyg  20263  zlmassa  20586  toprntopon  21528  tgclb  21573  iscldtop  21698  isnrm2  21961  isnrm3  21962  discmp  22001  dfconn2  22022  2ndcsb  22052  dis2ndc  22063  loclly  22090  unisngl  22130  locfindis  22133  iskgen2  22151  dfac14  22221  kqtop  22348  kqt0  22349  kqreg  22354  kqnrm  22355  hmpher  22387  hmphsymb  22389  hmph0  22398  kqhmph  22422  ist1-5lem  22423  elmptrab2  22431  isfil2  22459  filunirn  22485  isufil2  22511  hausflim  22584  isfcls  22612  alexsubALT  22654  istgp2  22694  ustbas  22831  xmetunirn  22942  dscmet  23177  dscopn  23178  isngp4  23216  zcld  23416  zlmclm  23715  iscmet2  23896  iundisj  24150  i1f1lem  24291  fta1b  24768  elply2  24791  elqaa  24916  aannenlem2  24923  wilth  25654  lgsne0  25917  2lgs  25989  2sqlem2  26000  ostth  26221  mptelee  26687  wrdupgr  26876  wrdumgr  26888  umgrislfupgr  26914  uspgrupgrushgr  26968  usgrumgruspgr  26971  usgruspgrb  26972  usgrislfuspgr  26975  uvtx01vtx  27185  wwlksnwwlksnon  27699  elwwlks2ons3  27739  clwwlkn1loopb  27826  eclclwwlkn1  27858  upgriseupth  27990  numclwwlkovh  28156  nmlno0lem  28574  isblo3i  28582  blocni  28586  hvsubeq0i  28844  hvaddcani  28846  bcseqi  28901  isch3  29022  norm1exi  29031  hhsssh  29050  shslubi  29166  dfch2  29188  pjoc1i  29212  pjchi  29213  shs00i  29231  chsscon3i  29242  chlejb1i  29257  chj00i  29268  shjshseli  29274  h1de2ctlem  29336  spanunsni  29360  cmcmi  29373  cmbr3i  29381  cmbr4i  29382  pj11i  29492  hosubeq0i  29607  dmadjrnb  29687  nmlnop0iALT  29776  lnopeq0i  29788  elunop2  29794  lnconi  29814  lncnopbd  29818  adjbdlnb  29865  adjbd1o  29866  adjeq0  29872  rnbra  29888  pjss1coi  29944  pjss2coi  29945  pjnormssi  29949  pjssdif2i  29955  pjssdif1i  29956  dfpjop  29963  pjinvari  29972  pjin2i  29974  pjci  29981  pjcmul1i  29982  pjcmul2i  29983  strb  30039  hstrbi  30047  mdsl1i  30102  atom1d  30134  chrelat2i  30146  cvbr4i  30148  cvexchi  30150  sumdmdi  30201  dmdbr4ati  30202  dmdbr5ati  30203  dmdbr6ati  30204  dmdbr7ati  30205  cdj3i  30222  eqtrb  30243  difeq  30287  iundisjf  30347  cnvoprabOLD  30466  fpwrelmap  30479  iundisjfi  30529  xrge0tsmsbi  30724  ccfldextdgrr  31114  issgon  31456  measbasedom  31535  oddpwdc  31686  eulerpartlemt  31703  ballotlem2  31820  ballotlemrinv  31865  bnj1533  32198  bnj983  32297  0nn0m1nnn0  32425  lfuhgr3  32440  spthcycl  32450  satfv1  32684  satf0op  32698  fmla0xp  32704  fmla1  32708  elmsta  32869  nepss  33022  dford5  33031  dfpo2  33065  dfon2  33111  distel  33122  elno2  33235  bdayfo  33256  fnimage  33464  altopthsn  33496  ellines  33687  rankeq1o  33706  opnrebl2  33743  df3nandALT1  33821  bj-animbi  33968  bj-dfbi6  33982  bj-consensus  33985  bj-falor2  33993  bj-bibibi  33994  bj-andnotim  33996  bj-cbval  34056  bj-cbvex  34057  bj-ssbeq  34060  bj-19.41al  34066  bj-sb56  34068  bj-eqs  34082  bj-cbvexw  34083  bj-sb  34095  bj-subst  34129  bj-dfnnf3  34162  bj-equs45fv  34209  bj-hbaeb2  34217  bj-hbnaeb  34219  bj-equsal  34225  bj-sbsb  34236  bj-moeub  34249  bj-csbsnlem  34305  bj-snsetex  34360  bj-snglex  34370  bj-1uplth  34404  bj-1uplex  34405  bj-2uplth  34418  bj-2uplex  34419  bj-bm1.3ii  34442  bj-restpw  34468  bj-restuni  34473  bj-discrmoore  34487  bj-snmooreb  34490  bj-elid6  34546  bj-eldiag2  34553  mptsnunlem  34716  topdifinf  34727  elxp8  34749  finxp1o  34770  wl-moae  34883  wl-exeq  34901  wl-aleq  34902  wl-nfeqfb  34903  wl-ax11-lem6  34949  volsupnfl  35064  cover2  35114  isbnd3  35184  cntotbnd  35196  heibor  35221  isfld2  35405  isfldidl  35468  orfa  35482  eqelb  35624  iss2  35723  issetssr  35865  n0el3  36007  prtlem16  36127  isltrn2N  37378  dffltz  39549  3cubes  39565  ismrc  39576  isnacs3  39585  rexzrexnn0  39679  eldioph4b  39686  dford3  39903  wopprc  39905  ttac  39911  pw2f1ocnv  39912  dfac11  39940  dfac21  39944  isnumbasabl  39984  isnumbasgrp  39985  dfacbasgrp  39986  aaitgo  40040  ifpbi1b  40145  rp-fakeimass  40154  rp-fakeanorass  40155  rp-isfinite5  40159  rp-isfinite6  40160  dfsucon  40165  snen1g  40166  iscard4  40175  rtrclex  40251  cnvtrrel  40305  rp-imass  40407  frege54cor0a  40499  isotone1  40688  isotone2  40689  gneispace  40774  k0004lem3  40789  grumnueq  40933  nanorxor  40947  nzss  40959  pm10.55  41011  pm11.57  41031  pm13.192  41052  pm13.194  41054  ipo0  41091  ifr0  41092  xpexb  41096  3impexpbicom  41123  com3rgbi  41158  pm2.43bgbi  41161  pm2.43cbi  41162  sb5ALT  41169  trsbc  41184  2pm13.193  41196  ax6e2ndeq  41203  2uasbanh  41205  eelT01  41355  eel0T1  41356  uunT1  41424  zfregs2VD  41485  equncomVD  41512  trsbcVD  41521  undif3VD  41526  2pm13.193VD  41547  ax6e2eqVD  41551  ax6e2ndeqVD  41553  2uasbanhVD  41555  ax6e2ndeqALT  41575  fompt  41761  mptssid  41819  elfzfzo  41850  allbutfi  41972  uzn0bi  42041  dvnprodlem3  42533  elaa2  42819  sge00  42958  elhoi  43124  ovn0  43148  ovolval4lem2  43232  confun  43475  afvfv0bi  43651  ffnafv  43670  afv2ndefb  43723  dfatafv2rnb  43726  afv2fv0b  43765  prpair  43961  sbcpr  43981  fpprel2  44202  sbgoldbmb  44247  mgm2mgm  44430  isringrng  44448  nnpw2pb  44944  0aryfvalel  44991  elsetrecs  45172  elpg  45186
  Copyright terms: Public domain W3C validator