Theorem impbii 125

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

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bicom  139  biid  170  2th  173  pm5.74  178  bitri  183  bibi2i  226  bi2.04  247  pm5.4  248  imdi  249  impexp  261  ancom  264  pm4.45im  332  dfbi2  386  anass  399  pm5.32  449  jcab  593  notnotnot  624  con2b  659  imnan  680  2false  691  pm5.21nii  694  pm4.8  697  oibabs  704  orcom  718  ioran  742  oridm  747  orbi2i  752  or12  756  pm4.44  769  ordi  806  andi  808  pm4.72  817  stdcndc  835  stdcndcOLD  836  stdcn  837  dcnn  838  pm4.82  940  rnlem  966  3jaob  1292  xoranor  1367  falantru  1393  3impexp  1425  3impexpbicom  1426  alcom  1466  19.26  1469  19.3h  1541  19.3  1542  19.21h  1545  19.43  1616  19.9h  1631  excom  1652  19.41h  1673  19.41  1674  equcom  1694  equsalh  1714  equsex  1716  cbvalv1  1739  cbvexv1  1740  cbvalh  1741  cbvexh  1743  sbbii  1753  sbh  1764  equs45f  1790  sb6f  1791  sbcof2  1798  sbequ8  1835  sbidm  1839  sb5rf  1840  sb6rf  1841  equvin  1851  sbimv  1881  cbvalvw  1907  cbvexvw  1908  sbalyz  1987  eu2  2058  eu3h  2059  eu5  2061  mo3h  2067  euan  2070  axext4  2149  cleqh  2266  r19.26  2592  ralcom3  2633  ceqsex  2764  gencbvex  2772  gencbvex2  2773  gencbval  2774  eqvinc  2849  pm13.183  2864  rr19.3v  2865  rr19.28v  2866  reu6  2915  reu3  2916  sbnfc2  3105  difdif  3247  ddifnel  3253  ddifstab  3254  ssddif  3356  difin  3359  uneqin  3373  indifdir  3378  undif3ss  3383  difrab  3396  un00  3455  undifss  3489  ssdifeq0  3491  ralidm  3509  ralf0  3512  ralm  3513  elpr2  3598  snidb  3606  difsnb  3716  preq12b  3750  preqsn  3755  axpweq  4150  exmidn0m  4180  exmidsssn  4181  exmid0el  4183  exmidel  4184  exmidundif  4185  exmidundifim  4186  sspwb  4194  unipw  4195  opm  4212  opth  4215  ssopab2b  4254  elon2  4354  unexb  4420  eusvnfb  4432  eusv2nf  4434  ralxfrALT  4445  uniexb  4451  iunpw  4458  sucelon  4480  unon  4488  sucprcreg  4526  opthreg  4533  ordsuc  4540  dcextest  4558  peano2b  4592  opelxp  4634  opthprc  4655  relop  4754  issetid  4758  xpid11  4827  elres  4920  iss  4930  issref  4986  xpmlem  5024  sqxpeq0  5027  ssrnres  5046  dfrel2  5054  relrelss  5130  fn0  5307  funssxp  5357  f00  5379  f0bi  5380  dffo2  5414  ffoss  5464  f1o00  5467  fo00  5468  fv3  5509  dff2  5629  dffo4  5633  dffo5  5634  fmpt  5635  ffnfv  5643  fsn  5657  fsn2  5659  isores1  5782  ssoprab2b  5899  eqfnov2  5949  cnvoprab  6202  reldmtpos  6221  mapsn  6656  mapsncnv  6661  mptelixpg  6700  elixpsn  6701  ixpsnf1o  6702  en0  6761  en1  6765  dom0  6804  exmidpw  6874  exmidpweq  6875  pw1fin  6876  undifdcss  6888  fidcenum  6921  djuexb  7009  ctssdc  7078  exmidomni  7106  exmidfodomr  7160  exmidontri  7195  exmidontri2or  7199  onntri3or  7201  onntri2or  7202  elni2  7255  ltbtwnnqq  7356  enq0ref  7374  elnp1st2nd  7417  elrealeu  7770  elreal2  7771  le2tri3i  8007  elnn0nn  9156  elnnnn0b  9158  elnnnn0c  9159  elnnz  9201  elnn0z  9204  elnnz1  9214  elz2  9262  eluz2b2  9541  elnn1uz2  9545  elpqb  9587  elioo4g  9870  eluzfz2b  9968  fzm  9973  elfz1end  9990  fzass4  9997  elfz1b  10025  fz01or  10046  nn0fz0  10054  fzolb  10088  fzom  10099  elfzo0  10117  fzo1fzo0n0  10118  elfzo0z  10119  elfzo1  10125  rexanuz  10930  rexuz3  10932  sqrt0rlem  10945  fisum0diag  11382  fprod0diagfz  11569  infssuzex  11882  isprm6  12079  oddpwdclemdc  12105  nnoddn2prmb  12194  4sqlem4  12322  ennnfone  12358  ctinfom  12361  ctinf  12363  tgclb  12705  xmetunirn  12998  2sqlem2  13591  bj-nnsn  13614  bdeq  13705  bdop  13757  bdunexb  13802  bj-2inf  13820  bj-nn0suc  13846  exmidsbth  13903  trirec0  13923  redc0  13936  reap0  13937