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  634  con2b  669  imnan  690  2false  701  pm5.21nii  704  pm4.8  707  oibabs  714  orcom  728  ioran  752  oridm  757  orbi2i  762  or12  766  pm4.44  779  ordi  816  andi  818  pm4.72  827  stdcndc  845  stdcndcOLD  846  stdcn  847  dcnn  848  pm4.82  950  rnlem  976  3jaob  1302  xoranor  1377  falantru  1403  3impexp  1437  3impexpbicom  1438  alcom  1478  19.26  1481  19.3h  1553  19.3  1554  19.21h  1557  19.43  1628  19.9h  1643  excom  1664  19.41h  1685  19.41  1686  equcom  1706  equsalh  1726  equsex  1728  cbvalv1  1751  cbvexv1  1752  cbvalh  1753  cbvexh  1755  sbbii  1765  sbh  1776  equs45f  1802  sb6f  1803  sbcof2  1810  sbequ8  1847  sbidm  1851  sb5rf  1852  sb6rf  1853  equvin  1863  sbimv  1893  cbvalvw  1919  cbvexvw  1920  sbalyz  1999  eu2  2070  eu3h  2071  eu5  2073  mo3h  2079  euan  2082  axext4  2161  cleqh  2277  r19.26  2603  ralcom3  2644  ceqsex  2775  gencbvex  2783  gencbvex2  2784  gencbval  2785  eqvinc  2860  pm13.183  2875  rr19.3v  2876  rr19.28v  2877  reu6  2926  reu3  2927  sbnfc2  3117  difdif  3260  ddifnel  3266  ddifstab  3267  ssddif  3369  difin  3372  uneqin  3386  indifdir  3391  undif3ss  3396  difrab  3409  un00  3469  undifss  3503  ssdifeq0  3505  ralidm  3523  ralf0  3526  ralm  3527  elpr2  3614  snidb  3622  difsnb  3735  preq12b  3770  preqsn  3775  axpweq  4171  exmidn0m  4201  exmidsssn  4202  exmid0el  4204  exmidel  4205  exmidundif  4206  exmidundifim  4207  sspwb  4216  unipw  4217  opm  4234  opth  4237  ssopab2b  4276  elon2  4376  unexb  4442  eusvnfb  4454  eusv2nf  4456  ralxfrALT  4467  uniexb  4473  iunpw  4480  onsucb  4502  unon  4510  sucprcreg  4548  opthreg  4555  ordsuc  4562  dcextest  4580  peano2b  4614  opelxp  4656  opthprc  4677  relop  4777  issetid  4781  xpid11  4850  elres  4943  iss  4953  issref  5011  xpmlem  5049  sqxpeq0  5052  ssrnres  5071  dfrel2  5079  relrelss  5155  fn0  5335  funssxp  5385  f00  5407  f0bi  5408  dffo2  5442  ffoss  5493  f1o00  5496  fo00  5497  fv3  5538  dff2  5660  dffo4  5664  dffo5  5665  fmpt  5666  ffnfv  5674  fsn  5688  fsn2  5690  isores1  5814  ssoprab2b  5931  eqfnov2  5981  cnvoprab  6234  reldmtpos  6253  mapsn  6689  mapsncnv  6694  mptelixpg  6733  elixpsn  6734  ixpsnf1o  6735  en0  6794  en1  6798  dom0  6837  exmidpw  6907  exmidpweq  6908  pw1fin  6909  undifdcss  6921  fidcenum  6954  djuexb  7042  ctssdc  7111  exmidomni  7139  nninfwlpo  7176  exmidfodomr  7202  exmidontri  7237  exmidontri2or  7241  onntri3or  7243  onntri2or  7244  dftap2  7249  exmidmotap  7259  elni2  7312  ltbtwnnqq  7413  enq0ref  7431  elnp1st2nd  7474  elrealeu  7827  elreal2  7828  le2tri3i  8065  elnn0nn  9217  elnnnn0b  9219  elnnnn0c  9220  elnnz  9262  elnn0z  9265  elnnz1  9275  elz2  9323  eluz2b2  9602  elnn1uz2  9606  elpqb  9648  elioo4g  9933  eluzfz2b  10032  fzm  10037  elfz1end  10054  fzass4  10061  elfz1b  10089  fz01or  10110  nn0fz0  10118  fzolb  10152  fzom  10163  elfzo0  10181  fzo1fzo0n0  10182  elfzo0z  10183  elfzo1  10189  rexanuz  10996  rexuz3  10998  sqrt0rlem  11011  fisum0diag  11448  fprod0diagfz  11635  infssuzex  11949  isprm6  12146  oddpwdclemdc  12172  nnoddn2prmb  12261  4sqlem4  12389  ennnfone  12425  ctinfom  12428  ctinf  12430  fnpr2ob  12758  dfgrp2  12901  dfgrp3m  12968  dfgrp3me  12969  isnsg3  13065  dvdsrzring  13463  tgclb  13535  xmetunirn  13828  2sqlem2  14432  bj-nnsn  14455  bdeq  14545  bdop  14597  bdunexb  14642  bj-2inf  14660  bj-nn0suc  14686  exmidsbth  14742  trirec0  14762  redc0  14775  reap0  14776  neap0mkv  14786