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-1 5  ax-2 6  ax-mp 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  330  dfbi2  383  anass  396  pm5.32  446  jcab  575  notnotnot  606  con2b  641  imnan  662  2false  673  pm5.21nii  676  pm4.8  679  oibabs  686  orcom  700  ioran  724  oridm  729  orbi2i  734  or12  738  pm4.44  751  ordi  788  andi  790  pm4.72  795  stdcndc  813  stdcndcOLD  814  stdcn  815  dcnn  816  pm4.82  917  rnlem  943  3jaob  1263  xoranor  1338  falantru  1364  3impexp  1396  3impexpbicom  1397  alcom  1437  19.26  1440  19.3h  1515  19.3  1516  19.21h  1519  19.43  1590  19.9h  1605  excom  1625  19.41h  1646  19.41  1647  equcom  1665  equsalh  1687  equsex  1689  cbvalh  1709  cbvexh  1711  sbbii  1721  sbh  1732  equs45f  1756  sb6f  1757  sbcof2  1764  sbequ8  1801  sbidm  1805  sb5rf  1806  sb6rf  1807  equvin  1817  sbimv  1847  sbalyz  1950  eu2  2019  eu3h  2020  eu5  2022  mo3h  2028  euan  2031  axext4  2099  cleqh  2214  r19.26  2532  ralcom3  2572  ceqsex  2695  gencbvex  2703  gencbvex2  2704  gencbval  2705  eqvinc  2778  pm13.183  2792  rr19.3v  2793  rr19.28v  2794  reu6  2842  reu3  2843  sbnfc2  3026  difdif  3167  ddifnel  3173  ddifstab  3174  ssddif  3276  difin  3279  uneqin  3293  indifdir  3298  undif3ss  3303  difrab  3316  un00  3375  undifss  3409  ssdifeq0  3411  ralidm  3429  ralf0  3432  ralm  3433  elpr2  3515  snidb  3521  difsnb  3629  preq12b  3663  preqsn  3668  axpweq  4055  exmidn0m  4084  exmidsssn  4085  exmid0el  4087  exmidel  4088  exmidundif  4089  exmidundifim  4090  sspwb  4098  unipw  4099  opm  4116  opth  4119  ssopab2b  4158  elon2  4258  unexb  4323  eusvnfb  4335  eusv2nf  4337  ralxfrALT  4348  uniexb  4354  iunpw  4361  sucelon  4379  unon  4387  sucprcreg  4424  opthreg  4431  ordsuc  4438  dcextest  4455  peano2b  4488  opelxp  4529  opthprc  4550  relop  4649  issetid  4653  xpid11  4722  elres  4813  iss  4823  issref  4879  xpmlem  4917  sqxpeq0  4920  ssrnres  4939  dfrel2  4947  relrelss  5023  fn0  5200  funssxp  5250  f00  5272  f0bi  5273  dffo2  5307  ffoss  5355  f1o00  5358  fo00  5359  fv3  5398  dff2  5518  dffo4  5522  dffo5  5523  fmpt  5524  ffnfv  5532  fsn  5546  fsn2  5548  isores1  5669  ssoprab2b  5782  eqfnov2  5832  cnvoprab  6085  reldmtpos  6104  mapsn  6538  mapsncnv  6543  mptelixpg  6582  elixpsn  6583  ixpsnf1o  6584  en0  6643  en1  6647  dom0  6685  exmidpw  6755  undifdcss  6764  fidcenum  6796  djuexb  6881  ctssdc  6950  exmidomni  6964  exmidfodomr  7008  elni2  7070  ltbtwnnqq  7171  enq0ref  7189  elnp1st2nd  7232  elrealeu  7564  elreal2  7565  le2tri3i  7795  elnn0nn  8923  elnnnn0b  8925  elnnnn0c  8926  elnnz  8968  elnn0z  8971  elnnz1  8981  elz2  9026  eluz2b2  9299  elnn1uz2  9303  elioo4g  9610  eluzfz2b  9706  fzm  9711  elfz1end  9728  fzass4  9735  elfz1b  9763  fz01or  9784  nn0fz0  9792  fzolb  9823  fzom  9834  elfzo0  9852  fzo1fzo0n0  9853  elfzo0z  9854  elfzo1  9860  rexanuz  10652  rexuz3  10654  sqrt0rlem  10667  fisum0diag  11102  infssuzex  11490  isprm6  11671  oddpwdclemdc  11696  ennnfone  11783  ctinfom  11786  ctinf  11788  tgclb  12077  xmetunirn  12347  bj-nnsn  12638  bdeq  12713  bdop  12765  bdunexb  12810  bj-2inf  12828  bj-nn0suc  12854  exmidsbth  12911