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  670  imnan  691  2false  702  pm5.21nii  705  pm4.8  708  oibabs  715  orcom  729  ioran  753  oridm  758  orbi2i  763  or12  767  pm4.44  780  ordi  817  andi  819  pm4.72  828  stdcndc  846  stdcndcOLD  847  stdcn  848  dcnn  849  pm4.82  952  rnlem  978  3jaob  1313  xoranor  1388  falantru  1414  3impexp  1448  3impexpbicom  1449  alcom  1492  19.26  1495  19.3h  1567  19.3  1568  19.21h  1571  19.43  1642  19.9h  1657  excom  1678  19.41h  1699  19.41  1700  equcom  1720  equsalh  1740  equsex  1742  cbvalv1  1765  cbvexv1  1766  cbvalh  1767  cbvexh  1769  sbbii  1779  sbh  1790  equs45f  1816  sb6f  1817  sbcof2  1824  sbequ8  1861  sbidm  1865  sb5rf  1866  sb6rf  1867  equvin  1877  sbimv  1908  cbvalvw  1934  cbvexvw  1935  sbalyz  2018  eu2  2089  eu3h  2090  eu5  2092  mo3h  2098  euan  2101  axext4  2180  cleqh  2296  r19.26  2623  ralcom3  2665  ceqsex  2801  gencbvex  2810  gencbvex2  2811  gencbval  2812  eqvinc  2887  pm13.183  2902  rr19.3v  2903  rr19.28v  2904  reu6  2953  reu3  2954  sbnfc2  3145  difdif  3289  ddifnel  3295  ddifstab  3296  ssddif  3398  difin  3401  uneqin  3415  indifdir  3420  undif3ss  3425  difrab  3438  un00  3498  undifss  3532  ssdifeq0  3534  ralidm  3552  ralf0  3554  ralm  3555  elpr2  3645  snidb  3653  difsnb  3766  preq12b  3801  preqsn  3806  axpweq  4205  exmidn0m  4235  exmidsssn  4236  exmid0el  4238  exmidel  4239  exmidundif  4240  exmidundifim  4241  sspwb  4250  unipw  4251  opm  4268  opth  4271  ssopab2b  4312  elon2  4412  unexb  4478  eusvnfb  4490  eusv2nf  4492  ralxfrALT  4503  uniexb  4509  iunpw  4516  onsucb  4540  unon  4548  sucprcreg  4586  opthreg  4593  ordsuc  4600  dcextest  4618  peano2b  4652  opelxp  4694  opthprc  4715  relop  4817  issetid  4821  xpid11  4890  elres  4983  iss  4993  issref  5053  xpmlem  5091  sqxpeq0  5094  ssrnres  5113  dfrel2  5121  relrelss  5197  fn0  5380  funssxp  5430  f00  5452  f0bi  5453  dffo2  5487  ffoss  5539  f1o00  5542  fo00  5543  fv3  5584  dff2  5709  dffo4  5713  dffo5  5714  fmpt  5715  ffnfv  5723  fsn  5737  fsn2  5739  isores1  5864  ssoprab2b  5983  eqfnov2  6034  cnvoprab  6301  reldmtpos  6320  mapsn  6758  mapsncnv  6763  mptelixpg  6802  elixpsn  6803  ixpsnf1o  6804  en0  6863  en1  6867  dom0  6908  exmidpw  6978  exmidpweq  6979  pw1fin  6980  exmidpw2en  6982  undifdcss  6993  residfi  7015  fidcenum  7031  djuexb  7119  ctssdc  7188  exmidomni  7217  nninfinfwlpo  7255  nninfwlpo  7256  exmidfodomr  7285  exmidontri  7324  exmidontri2or  7328  onntri3or  7330  onntri2or  7331  dftap2  7336  exmidmotap  7346  elni2  7400  ltbtwnnqq  7501  enq0ref  7519  elnp1st2nd  7562  elrealeu  7915  elreal2  7916  le2tri3i  8154  elnn0nn  9310  elnnnn0b  9312  elnnnn0c  9313  elnnz  9355  elnn0z  9358  elnnz1  9368  elz2  9416  eluz2b2  9696  elnn1uz2  9700  elpqb  9743  elioo4g  10028  eluzfz2b  10127  fzm  10132  elfz1end  10149  fzass4  10156  elfz1b  10184  fz01or  10205  nn0fz0  10213  fzolb  10248  fzom  10259  elfzo0  10277  fzo1fzo0n0  10278  elfzo0z  10279  elfzo1  10285  infssuzex  10342  wrdexb  10966  0wrd0  10980  rexanuz  11172  rexuz3  11174  sqrt0rlem  11187  fisum0diag  11625  fprod0diagfz  11812  isprm6  12342  oddpwdclemdc  12368  nnoddn2prmb  12458  4sqlem4  12588  4sqexercise1  12594  ennnfone  12669  ctinfom  12672  ctinf  12674  fnpr2ob  13044  dfgrp2  13231  dfgrp3m  13303  dfgrp3me  13304  isnsg3  13415  invghm  13537  dvdsrzring  14237  zrhval  14251  tgclb  14409  xmetunirn  14702  dich0  14996  elply2  15079  2sqlem2  15464  bj-nnsn  15487  bdeq  15577  bdop  15629  bdunexb  15674  bj-2inf  15692  bj-nn0suc  15718  nnnninfen  15776  exmidsbth  15781  trirec0  15801  redc0  15814  reap0  15815  cndcap  15816  neap0mkv  15826