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  607  notnotnot  639  con2b  675  imnan  696  2false  708  pm5.21nii  711  pm4.8  714  oibabs  721  orcom  735  ioran  759  oridm  764  orbi2i  769  or12  773  pm4.44  786  ordi  823  andi  825  pm4.72  834  stdcndc  852  stdcndcOLD  853  stdcn  854  dcnn  855  pm4.82  958  rnlem  984  3jaob  1338  xoranor  1421  falantru  1447  3impexp  1482  3impexpbicom  1483  alcom  1526  19.26  1529  19.3h  1601  19.3  1602  19.21h  1605  19.43  1676  19.9h  1691  excom  1712  19.41h  1733  19.41  1734  equcom  1754  equsalh  1774  equsex  1776  cbvalv1  1799  cbvexv1  1800  cbvalh  1801  cbvexh  1803  sbbii  1813  sbh  1824  equs45f  1850  sb6f  1851  sbcof2  1858  sbequ8  1895  sbidm  1899  sb5rf  1900  sb6rf  1901  equvin  1911  sbimv  1942  cbvalvw  1968  cbvexvw  1969  sbalyz  2052  eu2  2124  eu3h  2125  eu5  2127  mo3h  2133  euan  2136  axext4  2215  cleqh  2331  r19.26  2659  ralcom3  2701  ceqsex  2841  gencbvex  2850  gencbvex2  2851  gencbval  2852  eqvinc  2929  pm13.183  2944  rr19.3v  2945  rr19.28v  2946  reu6  2995  reu3  2996  sbnfc2  3188  difdif  3332  ddifnel  3338  ddifstab  3339  ssddif  3441  difin  3444  uneqin  3458  indifdir  3463  undif3ss  3468  difrab  3481  un00  3541  undifss  3575  ssdifeq0  3577  ralidm  3595  ralf0  3597  ralm  3598  elpr2  3691  snidb  3699  rabsnifsb  3737  difsnb  3816  preq12b  3853  preqsn  3858  axpweq  4261  exmidn0m  4291  exmidsssn  4292  exmid0el  4294  exmidel  4295  exmidundif  4296  exmidundifim  4297  sspwb  4308  unipw  4309  opm  4326  opth  4329  ssopab2b  4371  elon2  4473  unexb  4539  eusvnfb  4551  eusv2nf  4553  ralxfrALT  4564  uniexb  4570  iunpw  4577  onsucb  4601  unon  4609  sucprcreg  4647  opthreg  4654  ordsuc  4661  dcextest  4679  peano2b  4713  opelxp  4755  opthprc  4777  relop  4880  issetid  4884  xpid11  4955  elres  5049  iss  5059  issref  5119  xpmlem  5157  sqxpeq0  5160  ssrnres  5179  dfrel2  5187  relrelss  5263  fn0  5452  funssxp  5504  f00  5528  f0bi  5529  dffo2  5563  ffoss  5616  f1o00  5620  fo00  5621  fv3  5662  dff2  5791  dffo4  5795  dffo5  5796  fmpt  5797  ffnfv  5805  fsn  5819  fsn2  5821  funop  5831  isores1  5955  ssoprab2b  6078  eqfnov2  6129  cnvoprab  6399  reldmtpos  6419  mapsn  6859  mapsncnv  6864  mptelixpg  6903  elixpsn  6904  ixpsnf1o  6905  en0  6969  en1  6973  modom  6994  dom0  7024  exmidpw  7100  exmidpweq  7101  pw1fin  7102  exmidpw2en  7104  undifdcss  7115  exmidssfi  7131  residfi  7139  fidcenum  7155  djuexb  7243  ctssdc  7312  exmidomni  7341  nninfinfwlpo  7379  nninfwlpo  7380  exmidfodomr  7415  iftrueb01  7441  exmidontri  7457  exmidontri2or  7461  onntri3or  7463  onntri2or  7464  dftap2  7470  exmidmotap  7480  elni2  7534  ltbtwnnqq  7635  enq0ref  7653  elnp1st2nd  7696  elrealeu  8049  elreal2  8050  le2tri3i  8288  elnn0nn  9444  elnnnn0b  9446  elnnnn0c  9447  elnnz  9489  elnn0z  9492  elnnz1  9502  elz2  9551  eluz2b2  9837  elnn1uz2  9841  elpqb  9884  elioo4g  10169  eluzfz2b  10268  fzm  10273  elfz1end  10290  fzass4  10297  elfz1b  10325  fz01or  10346  nn0fz0  10354  fzolb  10389  fzom  10400  elfzo0  10421  fzo1fzo0n0  10423  elfzo0z  10424  elfzo1  10431  infssuzex  10494  hash2en  11108  wrdexb  11129  0wrd0  11143  rexanuz  11566  rexuz3  11568  sqrt0rlem  11581  fisum0diag  12020  fprod0diagfz  12207  isprm6  12737  oddpwdclemdc  12763  nnoddn2prmb  12853  4sqlem4  12983  4sqexercise1  12989  ennnfone  13064  ctinfom  13067  ctinf  13069  fnpr2ob  13441  dfgrp2  13628  dfgrp3m  13700  dfgrp3me  13701  isnsg3  13812  invghm  13934  dvdsrzring  14636  zrhval  14650  tgclb  14808  xmetunirn  15101  dich0  15395  elply2  15478  2sqlem2  15863  umgrislfupgrenlem  16000  umgrislfupgrdom  16001  uspgrupgrushgr  16052  usgrumgruspgr  16055  usgruspgrben  16056  usgrislfuspgrdom  16060  clwwlkn1loopb  16290  bj-nnsn  16380  bdeq  16469  bdop  16521  bdunexb  16566  bj-2inf  16584  bj-nn0suc  16610  pw1dceq  16656  nnnninfen  16674  exmidsbth  16679  trirec0  16699  redc0  16713  reap0  16714  cndcap  16715  neap0mkv  16725