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  603  notnotnot  635  con2b  671  imnan  692  2false  703  pm5.21nii  706  pm4.8  709  oibabs  716  orcom  730  ioran  754  oridm  759  orbi2i  764  or12  768  pm4.44  781  ordi  818  andi  820  pm4.72  829  stdcndc  847  stdcndcOLD  848  stdcn  849  dcnn  850  pm4.82  953  rnlem  979  3jaob  1315  xoranor  1397  falantru  1423  3impexp  1458  3impexpbicom  1459  alcom  1502  19.26  1505  19.3h  1577  19.3  1578  19.21h  1581  19.43  1652  19.9h  1667  excom  1688  19.41h  1709  19.41  1710  equcom  1730  equsalh  1750  equsex  1752  cbvalv1  1775  cbvexv1  1776  cbvalh  1777  cbvexh  1779  sbbii  1789  sbh  1800  equs45f  1826  sb6f  1827  sbcof2  1834  sbequ8  1871  sbidm  1875  sb5rf  1876  sb6rf  1877  equvin  1887  sbimv  1918  cbvalvw  1944  cbvexvw  1945  sbalyz  2028  eu2  2099  eu3h  2100  eu5  2102  mo3h  2108  euan  2111  axext4  2190  cleqh  2306  r19.26  2633  ralcom3  2675  ceqsex  2812  gencbvex  2821  gencbvex2  2822  gencbval  2823  eqvinc  2900  pm13.183  2915  rr19.3v  2916  rr19.28v  2917  reu6  2966  reu3  2967  sbnfc2  3158  difdif  3302  ddifnel  3308  ddifstab  3309  ssddif  3411  difin  3414  uneqin  3428  indifdir  3433  undif3ss  3438  difrab  3451  un00  3511  undifss  3545  ssdifeq0  3547  ralidm  3565  ralf0  3567  ralm  3568  elpr2  3660  snidb  3668  difsnb  3782  preq12b  3817  preqsn  3822  axpweq  4223  exmidn0m  4253  exmidsssn  4254  exmid0el  4256  exmidel  4257  exmidundif  4258  exmidundifim  4259  sspwb  4268  unipw  4269  opm  4286  opth  4289  ssopab2b  4331  elon2  4431  unexb  4497  eusvnfb  4509  eusv2nf  4511  ralxfrALT  4522  uniexb  4528  iunpw  4535  onsucb  4559  unon  4567  sucprcreg  4605  opthreg  4612  ordsuc  4619  dcextest  4637  peano2b  4671  opelxp  4713  opthprc  4734  relop  4836  issetid  4840  xpid11  4910  elres  5004  iss  5014  issref  5074  xpmlem  5112  sqxpeq0  5115  ssrnres  5134  dfrel2  5142  relrelss  5218  fn0  5405  funssxp  5455  f00  5479  f0bi  5480  dffo2  5514  ffoss  5566  f1o00  5570  fo00  5571  fv3  5612  dff2  5737  dffo4  5741  dffo5  5742  fmpt  5743  ffnfv  5751  fsn  5765  fsn2  5767  funop  5776  isores1  5896  ssoprab2b  6015  eqfnov2  6066  cnvoprab  6333  reldmtpos  6352  mapsn  6790  mapsncnv  6795  mptelixpg  6834  elixpsn  6835  ixpsnf1o  6836  en0  6900  en1  6904  dom0  6950  exmidpw  7020  exmidpweq  7021  pw1fin  7022  exmidpw2en  7024  undifdcss  7035  residfi  7057  fidcenum  7073  djuexb  7161  ctssdc  7230  exmidomni  7259  nninfinfwlpo  7297  nninfwlpo  7298  exmidfodomr  7328  iftrueb01  7354  exmidontri  7370  exmidontri2or  7374  onntri3or  7376  onntri2or  7377  dftap2  7383  exmidmotap  7393  elni2  7447  ltbtwnnqq  7548  enq0ref  7566  elnp1st2nd  7609  elrealeu  7962  elreal2  7963  le2tri3i  8201  elnn0nn  9357  elnnnn0b  9359  elnnnn0c  9360  elnnz  9402  elnn0z  9405  elnnz1  9415  elz2  9464  eluz2b2  9744  elnn1uz2  9748  elpqb  9791  elioo4g  10076  eluzfz2b  10175  fzm  10180  elfz1end  10197  fzass4  10204  elfz1b  10232  fz01or  10253  nn0fz0  10261  fzolb  10296  fzom  10307  elfzo0  10328  fzo1fzo0n0  10329  elfzo0z  10330  elfzo1  10336  infssuzex  10398  hash2en  11010  wrdexb  11028  0wrd0  11042  rexanuz  11374  rexuz3  11376  sqrt0rlem  11389  fisum0diag  11827  fprod0diagfz  12014  isprm6  12544  oddpwdclemdc  12570  nnoddn2prmb  12660  4sqlem4  12790  4sqexercise1  12796  ennnfone  12871  ctinfom  12874  ctinf  12876  fnpr2ob  13247  dfgrp2  13434  dfgrp3m  13506  dfgrp3me  13507  isnsg3  13618  invghm  13740  dvdsrzring  14440  zrhval  14454  tgclb  14612  xmetunirn  14905  dich0  15199  elply2  15282  2sqlem2  15667  bj-nnsn  15808  bdeq  15897  bdop  15949  bdunexb  15994  bj-2inf  16012  bj-nn0suc  16038  nnnninfen  16099  exmidsbth  16104  trirec0  16124  redc0  16137  reap0  16138  cndcap  16139  neap0mkv  16149