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

Step	Hyp	Ref	Expression
1		impbii.1	. 2 ⊢ (𝜑 → 𝜓)
2		impbii.2	. 2 ⊢ (𝜓 → 𝜑)
3		impbi 211	. 2 ⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → (𝜑 ↔ 𝜓)))
4	1, 2, 3	mp2 9	1 ⊢ (𝜑 ↔ 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bicom  225  biid  264  2th  267  pm5.74  273  bitri  278  notnotb  318  con34b  319  notbi  322  bibi2i  340  con1b  361  con2b  362  bi2.04  392  imdi  394  pm4.8  398  pm4.81  399  impexp  456  ancom  466  anass  474  jcab  527  abab  840  impimprbi  842  orcom  884  dfor2  915  oridm  918  orbi2i  926  or12  934  pm4.72  964  oibabs  966  jaob  976  pm4.44  1012  pm4.79  1021  andi  1025  pm4.82  1041  cases2ALT  1064  consensus  1068  3impexp  1377  nanass  1539  tbw-bijust  1730  tbw-negdf  1731  19.26  1902  19.35  1909  19.21v  1971  19.23v  1974  19.41v  1981  19.3v  2014  19.9v  2016  equcom  2050  cbvalw  2067  alcomw  2077  excomw  2078  exexw  2085  sbbii  2112  sban  2116  sbv  2124  sbrimvw  2127  alcom  2195  19.3  2238  19.41  2271  sbalex  2278  equsexv  2302  sbim  2336  cbvalv1  2370  cbval  2427  equsex  2447  aecom  2456  equs45f  2488  dfsb1  2510  dfsb2  2522  sb6f  2526  dfmoeu  2560  moabs  2568  mo3  2589  mo4  2591  exmoeu  2606  moanimlem  2643  euan  2646  euanv  2649  2mo  2673  2eu6  2681  euae  2684  axextb  2735  eqcom  2767  nebi  3035  r19.35  3120  r19.26  3122  r19.21v  3187  gencbvex  3506  gencbvex2  3507  pm13.183  3619  rr19.3v  3620  rr19.28v  3621  euxfr2w  3677  euxfr2  3679  reu6  3683  reu3  3684  reuan  3844  sspss  4028  complss  4086  dfss2  4093  unineq  4232  uneqin  4233  difrab  4262  un00  4356  vvin  4358  sbnfc2  4396  ssdifeq0  4441  r19.2zb  4455  ralidmw  4471  ralidm  4472  pwidb  4579  snidb  4618  rabsnifsb  4679  tppreqb  4764  difsnb  4765  sssn  4781  preq12b  4804  pwpw0  4830  unissint  4931  uniintsn  4944  iununi  5058  al0ssb  5261  intex  5305  intnex  5306  axpweq  5312  iin0  5324  nfcvb  5338  eusvnfb  5355  eusv2nf  5357  ralxfrALT  5377  sspwb  5417  unipw  5418  opnz  5442  opth  5445  sbcop1  5458  opeqsng  5475  propeqop  5479  opthwiener  5487  opthhausdorff  5490  opthhausdorff0  5491  rexopabb  5502  ssopab2bw  5522  ssopab2b  5524  pwssun  5543  opelxp  5687  opthprc  5715  relsnb  5781  relop  5829  issetid  5833  xpid11  5915  elinxp  6010  eldmeldmressn  6016  iss  6029  iresn0n0  6048  asymref2  6113  xpnz  6152  xpdifid  6161  xpdifcnvepel  6162  ssrnres  6172  dfrel2  6183  relcnvtrg  6271  resssxp  6275  relrelss  6278  unixp0  6289  reuop  6299  dfpo2  6302  fn0  6675  funssxp  6743  f00  6769  f0bi  6770  dffo2  6805  f1o00  6865  fo00  6866  fv3  6908  dffn5  6948  dff2  7104  dff3  7105  dffo4  7108  dffo5  7109  exfo  7110  fmpt  7115  fompt  7123  ffnfv  7124  fsn  7141  fsn2  7142  funop  7158  funsneqopb  7161  isores1  7346  ssoprab2b  7493  eqoprab2bw  7494  eqfnov2  7554  unexb  7767  uniexb  7782  pwexb  7784  iunpw  7789  ordeleqon  7800  dford5  7802  onintrab  7814  ordsuc  7829  unon  7846  onuninsuci  7855  ordzsl  7860  onzsl  7861  f1oexbi  7944  ffoss  7962  1st2ndb  8045  frxp3  8174  suppssov1  8221  suppssov2  8222  suppssfv  8226  reldmtpos  8258  dfrecs3  8387  omopthi  8677  brinxper  8754  ecopover  8849  fsetexb  8893  mapsncnv  8928  mptelixpg  8970  elixpsn  8972  ixpsnf1o  8973  bren2  9017  en0  9052  en0ALT  9053  en0r  9054  en1  9058  en1b  9059  sbthb  9124  dom0  9131  canth2  9156  onfin2  9239  sdom1  9248  1sdom2dom  9252  fineqv  9265  unfilem1  9304  unfib  9308  pwfir  9315  pwfi  9317  fiint  9325  residfi  9334  unifpw  9351  wofib  9546  sucprcreg  9607  sucprcregOLD  9608  opthreg  9626  suc11reg  9627  infeq5  9645  rankwflemb  9807  rankwflembOLD  9808  r1elss  9821  pwwf  9822  unwf  9825  uniwf  9835  rankonid  9846  rankr1id  9885  rankuni  9886  rankxplim3  9905  elhf4  9919  elhf3OLD  9930  scott0b  9944  scott0OLD  9945  karden  9966  kardenOLD  9967  djuexb  9997  isnum3  10042  oncard  10048  card1  10056  cardlim  10060  cardmin2  10087  pm54.43lem  10088  ween  10121  acnnum  10138  alephsuc2  10166  alephgeom  10168  iscard3  10179  dfac3  10207  dfac4  10208  dfac5lem3  10211  dfac5  10214  dfac2  10217  dfac8  10221  dfac9  10222  dfacacn  10227  dfac13  10228  dfac12r  10232  dfac12k  10233  kmlem2  10237  kmlem13  10248  djuinf  10274  ackbij2  10327  cflim2  10348  isfin4-2  10399  isfin4p1  10400  isf33lem  10451  compsscnv  10456  fin1a2lem6  10490  domtriom  10528  ac9  10568  ac9s  10578  fodomb  10612  brdom3  10614  brdom5  10615  brdom4  10616  brdom7disj  10617  brdom6disj  10618  iunfo  10630  sdomsdomcard  10651  gch2  10767  gch3  10768  eltsk2g  10843  grutsk  10914  ordpipq  11034  ltbtwnnq  11070  mappsrpr  11200  map2psrpr  11202  elreal2  11224  le2tri3i  11447  elnn0nn  12655  elnnnn0b  12657  elnnnn0c  12658  elnnz  12710  elnn0z  12713  elz2  12718  elnnz1  12729  0nn0m1nnn0  12760  eluz2b2  13055  elnn1uz2  13059  elpqb  13111  elioo4g  13544  eluzfz2b  13673  fzn0  13678  elfz1end  13695  fzass4  13703  elfz1b  13734  nn0fz0  13766  fzolb  13807  fzon0  13819  elfzo0  13842  elfzo0z  13843  elfzo1  13854  fzo1fzo0n0  13857  om2uzrani  14102  nn0opthi  14421  hashkf  14483  isfinite4  14513  hashprb  14548  hashf1  14609  elss2prb  14640  iswrdb  14672  wrdexb  14677  0wrd0  14692  s3rex  15110  wrdl3s3  15124  cotr2g  15138  trclun  15176  rexanuz  15522  rexuz3  15525  fsum0diag  15952  fprod0diag  16162  divalgmod  16585  sadcp1  16634  isprm6  16899  nnoddn2prmb  17000  4sqlem4  17139  fnpr2ob  17739  mreunirn  17780  isdrs2  18489  isacs5  18731  isacs4  18732  isacs3  18733  dfgrp2  19182  dfgrp3  19258  dfgrp3e  19259  isnsg3  19379  gicer  19500  oppgmndb  19578  oppggrpb  19581  pmtrfb  19688  invghm  20056  isringrng  20525  dfring2  20526  opprrngb  20585  opprringb  20587  ricer  20765  isnzr2hash  20779  isdomn4  20976  isdrng2  21006  abvn0b  21102  gzrngunit  21748  dvdsrzring  21776  zringunit  21781  zlmlmod  21837  cygth  21886  frgpcyg  21888  zlmassa  22220  toprntopon  23252  tgclb  23297  iscldtop  23422  isnrm2  23685  isnrm3  23686  discmp  23725  dfconn2  23746  2ndcsb  23776  dis2ndc  23788  loclly  23815  unisngl  23855  locfindis  23858  iskgen2  23876  dfac14  23946  kqtop  24073  kqt0  24074  kqreg  24079  kqnrm  24080  hmpher  24112  hmphsymb  24114  hmph0  24123  kqhmph  24147  ist1-5lem  24148  elmptrab2  24156  isfil2  24184  filunirn  24210  isufil2  24236  hausflim  24309  isfcls  24337  alexsubALT  24379  istgp2  24419  ustbas  24555  xmetunirn  24665  dscmet  24900  dscopn  24901  isngp4  24940  zcld  25142  zlmclm  25442  iscmet2  25624  iundisj  25878  i1f1lem  26019  fta1b  26499  elply2  26523  elqaa  26654  aannenlem2  26665  wilth  27407  lgsne0  27671  2lgs  27743  2sqlem2  27754  ostth  27975  elno2  28020  bdayfo  28043  elons2  28653  eln0s2  28752  eln0s  28756  elzn0s  28793  eln0zs  28795  elnnzs  28796  remulscllem1  28895  mpteleeOLD  29482  wrdupgr  29672  wrdumgr  29684  umgrislfupgr  29710  lfuhgr3  29737  uspgrupgrushgr  29769  usgrumgruspgr  29772  usgruspgrb  29773  usgrislfuspgr  29777  uvtx01vtx  29987  pthspthcyc  30400  spthcycl  30401  wwlksnwwlksnon  30513  elwwlks2ons3  30553  clwwlkn1loopb  30643  eclclwwlkn1  30675  upgriseupth  30817  numclwwlkovh  30983  nmlno0lem  31404  isblo3i  31412  blocni  31416  hvsubeq0i  31674  hvaddcani  31676  bcseqi  31731  isch3  31852  norm1exi  31861  hhsssh  31880  shslubi  31996  dfch2  32018  pjoc1i  32042  pjchi  32043  shs00i  32061  chsscon3i  32072  chlejb1i  32087  chj00i  32098  shjshseli  32104  h1de2ctlem  32166  spanunsni  32190  cmcmi  32203  cmbr3i  32211  cmbr4i  32212  pj11i  32322  hosubeq0i  32437  dmadjrnb  32517  nmlnop0iALT  32606  lnopeq0i  32618  elunop2  32624  lnconi  32644  lncnopbd  32648  adjbdlnb  32695  adjbd1o  32696  adjeq0  32702  rnbra  32718  pjss1coi  32774  pjss2coi  32775  pjnormssi  32779  pjssdif2i  32785  pjssdif1i  32786  dfpjop  32793  pjinvari  32802  pjin2i  32804  pjci  32811  pjcmul1i  32812  pjcmul2i  32813  strb  32869  hstrbi  32877  mdsl1i  32932  atom1d  32964  chrelat2i  32976  cvbr4i  32978  cvexchi  32980  sumdmdi  33031  dmdbr4ati  33032  dmdbr5ati  33033  dmdbr6ati  33034  dmdbr7ati  33035  cdj3i  33052  eqtrb  33121  difeq  33165  iundisjf  33234  fpwrelmap  33375  iundisjfi  33438  xrge0tsmsbi  33685  dflring2  34075  dfufd2  34132  0mplrim  34196  ccfldextdgrr  34354  issgon  34805  measbasedom  34885  oddpwdc  35036  eulerpartlemt  35053  ballotlem2  35171  ballotlemrinv  35216  bnj1533  35532  bnj983  35631  reu6f  35759  rmo6  35760  r1omhfb  35794  dfac15  35813  dfac16  35814  fineqvomonb  35847  fineqvnttrclse  35852  r1omhfbregs  35865  fineqvr1ombregs  35866  kardeq0  35884  karddom  35889  kardsdom  35890  kardexen  35891  satfv1  36218  satf0op  36232  fmla0xp  36238  fmla1  36242  elmsta  36403  antnestlaw1  36546  antnestlaw2  36547  antnestlaw3  36548  nepss  36579  dfon2  36650  distel  36661  fnimage  36787  altopthsn  36822  ellines  37013  rankeq1o  37028  opnrebl2  37205  df3nandALT1  37283  ttc00  37392  ttcwf  37408  ttcwf2  37409  ttcexbi  37417  ttc0el  37419  bj-animbi  37524  bj-dfbi6  37541  bj-consensus  37544  bj-falor2  37551  bj-bibibi  37552  bj-andnotim  37554  bj-alextruim  37632  bj-exextruan  37633  bj-ssbeq  37648  bj-19.41al  37654  bj-subst  37656  bj-eqs  37671  bj-cbvexw  37672  bj-sb  37685  bj-substax12  37722  bj-dfnnf3  37779  bj-equs45fv  37819  bj-hbaeb2  37826  bj-hbnaeb  37828  bj-equsal  37834  bj-sbsb  37845  bj-moeub  37857  bj-csbsnlem  37911  bj-snsetex  37972  bj-snglex  37982  bj-1uplth  38016  bj-1uplex  38017  bj-2uplth  38030  bj-2uplex  38031  bj-bm1.3ii  38087  bj-restpw  38121  bj-restuni  38126  bj-discrmoore  38140  bj-snmooreb  38143  bj-elid6  38200  bj-eldiag2  38207  mptsnunlem  38370  topdifinf  38381  elxp8  38403  finxp1o  38424  wl-moae  38557  wl-exeq  38575  wl-aleq  38576  wl-nfeqfb  38577  volsupnfl  38692  cover2  38758  isbnd3  38827  cntotbnd  38839  heibor  38864  isfld2  39048  isfldidl  39111  orfa  39125  eqbrb  39280  eqelb  39282  iss2  39385  issetssr  39624  n0el3  39777  detlem  39927  petlem  39956  eldisjs6  39981  prtlem16  40035  isltrn2N  41286  aks6d1c2p2  43278  aks6d1c6isolem3  43335  sn-iotalem  43384  dffltz  43779  eu6w  43796  3cubes  43809  ismrc  43821  isnacs3  43830  rexzrexnn0  43920  eldioph4b  43927  dford3  44144  wopprc  44146  ttac  44152  pw2f1ocnv  44153  dfac11  44173  dfac21  44177  isnumbasabl  44217  isnumbasgrp  44218  dfacbasgrp  44219  aaitgo  44273  dflim5  44440  nvocnvb  44532  dfno2  44538  ifpbi1b  44613  rp-fakeimass  44622  rp-fakeanorass  44623  rp-isfinite5  44627  rp-isfinite6  44628  dfsucon  44633  snen1g  44634  iscard4  44643  rtrclex  44726  cnvtrrel  44779  frege54cor0a  44972  isotone1  45157  isotone2  45158  gneispace  45243  k0004lem3  45258  grumnueq  45380  ismnushort  45394  nanorxor  45398  nzss  45410  pm10.55  45462  pm11.57  45482  pm13.192  45503  pm13.194  45505  ipo0  45540  ifr0  45541  xpexb  45544  3impexpbicom  45571  com3rgbi  45605  pm2.43bgbi  45608  pm2.43cbi  45609  sb5ALT  45616  trsbc  45631  2pm13.193  45643  ax6e2ndeq  45650  2uasbanh  45652  eelT01  45801  eel0T1  45802  uunT1  45870  zfregs2VD  45931  equncomVD  45958  trsbcVD  45967  undif3VD  45972  2pm13.193VD  45993  ax6e2eqVD  45997  ax6e2ndeqVD  45999  2uasbanhVD  46001  ax6e2ndeqALT  46021  tcfr  46061  mptssid  46361  elfzfzo  46401  allbutfi  46512  uzn0bi  46577  dvnprodlem3  47066  elaa2  47352  sge00  47494  elhoi  47660  ovn0  47684  ovolval4lem2  47768  wrddin2  48006  chndin2  48011  chnrin2  48016  confun  48117  afvfv0bi  48330  ffnafv  48349  afv2ndefb  48402  dfatafv2rnb  48405  afv2fv0b  48444  prpair  48691  sbcpr  48711  fpprel2  48947  sbgoldbmb  48992  vopnbgrelself  49061  isgrtri  49149  stgr1  49167  mgm2mgm  49432  nnpw2pb  49807  0aryfvalel  49854  mo0sn  50035  resinsnlem  50092  elixpmpt  50112  homf0  50231  isoval2  50257  oppccicb  50273  oppcciceq  50274  funcf2lem2  50304  initc  50314  isinito2  50742  isinito3  50743  termc  50762  dftermc3  50774  elsetrecs  50976  elpg  50990