Theorem impbii 126

Description: Infer an equivalence from an implication and its converse. (Contributed by NM, 5-Aug-1993.)

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		bi3 119	. 2 ⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → (𝜑 ↔ 𝜓)))
4	1, 2, 3	mp2 16	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bicom  140  biid  171  2th  174  pm5.74  179  bitri  184  bibi2i  227  bi2.04  248  pm5.4  249  imdi  250  impexp  263  ancom  266  pm4.45im  334  dfbi2  388  anass  401  pm5.32  453  jcab  605  notnotnot  637  con2b  673  imnan  694  2false  706  pm5.21nii  709  pm4.8  712  oibabs  719  orcom  733  ioran  757  oridm  762  orbi2i  767  or12  771  pm4.44  784  ordi  821  andi  823  pm4.72  832  stdcndc  850  stdcndcOLD  851  stdcn  852  dcnn  853  pm4.82  956  rnlem  982  3jaob  1336  xoranor  1419  falantru  1445  3impexp  1480  3impexpbicom  1481  alcom  1524  19.26  1527  19.3h  1599  19.3  1600  19.21h  1603  19.43  1674  19.9h  1689  excom  1710  19.41h  1731  19.41  1732  equcom  1752  equsalh  1772  equsex  1774  cbvalv1  1797  cbvexv1  1798  cbvalh  1799  cbvexh  1801  sbbii  1811  sbh  1822  equs45f  1848  sb6f  1849  sbcof2  1856  sbequ8  1893  sbidm  1897  sb5rf  1898  sb6rf  1899  equvin  1909  sbimv  1940  cbvalvw  1966  cbvexvw  1967  sbalyz  2050  eu2  2122  eu3h  2123  eu5  2125  mo3h  2131  euan  2134  axext4  2213  cleqh  2329  r19.26  2657  ralcom3  2699  ceqsex  2838  gencbvex  2847  gencbvex2  2848  gencbval  2849  eqvinc  2926  pm13.183  2941  rr19.3v  2942  rr19.28v  2943  reu6  2992  reu3  2993  sbnfc2  3185  difdif  3329  ddifnel  3335  ddifstab  3336  ssddif  3438  difin  3441  uneqin  3455  indifdir  3460  undif3ss  3465  difrab  3478  un00  3538  undifss  3572  ssdifeq0  3574  ralidm  3592  ralf0  3594  ralm  3595  elpr2  3688  snidb  3696  difsnb  3811  preq12b  3848  preqsn  3853  axpweq  4255  exmidn0m  4285  exmidsssn  4286  exmid0el  4288  exmidel  4289  exmidundif  4290  exmidundifim  4291  sspwb  4302  unipw  4303  opm  4320  opth  4323  ssopab2b  4365  elon2  4467  unexb  4533  eusvnfb  4545  eusv2nf  4547  ralxfrALT  4558  uniexb  4564  iunpw  4571  onsucb  4595  unon  4603  sucprcreg  4641  opthreg  4648  ordsuc  4655  dcextest  4673  peano2b  4707  opelxp  4749  opthprc  4770  relop  4872  issetid  4876  xpid11  4947  elres  5041  iss  5051  issref  5111  xpmlem  5149  sqxpeq0  5152  ssrnres  5171  dfrel2  5179  relrelss  5255  fn0  5443  funssxp  5495  f00  5519  f0bi  5520  dffo2  5554  ffoss  5606  f1o00  5610  fo00  5611  fv3  5652  dff2  5781  dffo4  5785  dffo5  5786  fmpt  5787  ffnfv  5795  fsn  5809  fsn2  5811  funop  5820  isores1  5944  ssoprab2b  6067  eqfnov2  6118  cnvoprab  6386  reldmtpos  6405  mapsn  6845  mapsncnv  6850  mptelixpg  6889  elixpsn  6890  ixpsnf1o  6891  en0  6955  en1  6959  dom0  7007  exmidpw  7081  exmidpweq  7082  pw1fin  7083  exmidpw2en  7085  undifdcss  7096  residfi  7118  fidcenum  7134  djuexb  7222  ctssdc  7291  exmidomni  7320  nninfinfwlpo  7358  nninfwlpo  7359  exmidfodomr  7393  iftrueb01  7419  exmidontri  7435  exmidontri2or  7439  onntri3or  7441  onntri2or  7442  dftap2  7448  exmidmotap  7458  elni2  7512  ltbtwnnqq  7613  enq0ref  7631  elnp1st2nd  7674  elrealeu  8027  elreal2  8028  le2tri3i  8266  elnn0nn  9422  elnnnn0b  9424  elnnnn0c  9425  elnnz  9467  elnn0z  9470  elnnz1  9480  elz2  9529  eluz2b2  9810  elnn1uz2  9814  elpqb  9857  elioo4g  10142  eluzfz2b  10241  fzm  10246  elfz1end  10263  fzass4  10270  elfz1b  10298  fz01or  10319  nn0fz0  10327  fzolb  10362  fzom  10373  elfzo0  10394  fzo1fzo0n0  10395  elfzo0z  10396  elfzo1  10403  infssuzex  10465  hash2en  11078  wrdexb  11096  0wrd0  11110  rexanuz  11514  rexuz3  11516  sqrt0rlem  11529  fisum0diag  11967  fprod0diagfz  12154  isprm6  12684  oddpwdclemdc  12710  nnoddn2prmb  12800  4sqlem4  12930  4sqexercise1  12936  ennnfone  13011  ctinfom  13014  ctinf  13016  fnpr2ob  13388  dfgrp2  13575  dfgrp3m  13647  dfgrp3me  13648  isnsg3  13759  invghm  13881  dvdsrzring  14582  zrhval  14596  tgclb  14754  xmetunirn  15047  dich0  15341  elply2  15424  2sqlem2  15809  umgrislfupgrenlem  15943  umgrislfupgrdom  15944  uspgrupgrushgr  15995  usgrumgruspgr  15998  usgruspgrben  15999  usgrislfuspgrdom  16003  bj-nnsn  16152  bdeq  16241  bdop  16293  bdunexb  16338  bj-2inf  16356  bj-nn0suc  16382  pw1dceq  16429  nnnninfen  16447  exmidsbth  16452  trirec0  16472  redc0  16485  reap0  16486  cndcap  16487  neap0mkv  16497