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  605  notnotnot  637  con2b  673  imnan  694  2false  706  pm5.21nii  709  pm4.8  712  oibabs  719  orcom  733  ioran  757  oridm  762  orbi2i  767  or12  771  pm4.44  784  ordi  821  andi  823  pm4.72  832  stdcndc  850  stdcndcOLD  851  stdcn  852  dcnn  853  pm4.82  956  rnlem  982  3jaob  1336  xoranor  1419  falantru  1445  3impexp  1480  3impexpbicom  1481  alcom  1524  19.26  1527  19.3h  1599  19.3  1600  19.21h  1603  19.43  1674  19.9h  1689  excom  1710  19.41h  1731  19.41  1732  equcom  1752  equsalh  1772  equsex  1774  cbvalv1  1797  cbvexv1  1798  cbvalh  1799  cbvexh  1801  sbbii  1811  sbh  1822  equs45f  1848  sb6f  1849  sbcof2  1856  sbequ8  1893  sbidm  1897  sb5rf  1898  sb6rf  1899  equvin  1909  sbimv  1940  cbvalvw  1966  cbvexvw  1967  sbalyz  2050  eu2  2122  eu3h  2123  eu5  2125  mo3h  2131  euan  2134  axext4  2213  cleqh  2329  r19.26  2657  ralcom3  2699  ceqsex  2838  gencbvex  2847  gencbvex2  2848  gencbval  2849  eqvinc  2926  pm13.183  2941  rr19.3v  2942  rr19.28v  2943  reu6  2992  reu3  2993  sbnfc2  3185  difdif  3329  ddifnel  3335  ddifstab  3336  ssddif  3438  difin  3441  uneqin  3455  indifdir  3460  undif3ss  3465  difrab  3478  un00  3538  undifss  3572  ssdifeq0  3574  ralidm  3592  ralf0  3594  ralm  3595  elpr2  3688  snidb  3696  difsnb  3810  preq12b  3847  preqsn  3852  axpweq  4254  exmidn0m  4284  exmidsssn  4285  exmid0el  4287  exmidel  4288  exmidundif  4289  exmidundifim  4290  sspwb  4301  unipw  4302  opm  4319  opth  4322  ssopab2b  4364  elon2  4466  unexb  4532  eusvnfb  4544  eusv2nf  4546  ralxfrALT  4557  uniexb  4563  iunpw  4570  onsucb  4594  unon  4602  sucprcreg  4640  opthreg  4647  ordsuc  4654  dcextest  4672  peano2b  4706  opelxp  4748  opthprc  4769  relop  4871  issetid  4875  xpid11  4946  elres  5040  iss  5050  issref  5110  xpmlem  5148  sqxpeq0  5151  ssrnres  5170  dfrel2  5178  relrelss  5254  fn0  5442  funssxp  5492  f00  5516  f0bi  5517  dffo2  5551  ffoss  5603  f1o00  5607  fo00  5608  fv3  5649  dff2  5778  dffo4  5782  dffo5  5783  fmpt  5784  ffnfv  5792  fsn  5806  fsn2  5808  funop  5817  isores1  5937  ssoprab2b  6060  eqfnov2  6111  cnvoprab  6378  reldmtpos  6397  mapsn  6835  mapsncnv  6840  mptelixpg  6879  elixpsn  6880  ixpsnf1o  6881  en0  6945  en1  6949  dom0  6995  exmidpw  7066  exmidpweq  7067  pw1fin  7068  exmidpw2en  7070  undifdcss  7081  residfi  7103  fidcenum  7119  djuexb  7207  ctssdc  7276  exmidomni  7305  nninfinfwlpo  7343  nninfwlpo  7344  exmidfodomr  7378  iftrueb01  7404  exmidontri  7420  exmidontri2or  7424  onntri3or  7426  onntri2or  7427  dftap2  7433  exmidmotap  7443  elni2  7497  ltbtwnnqq  7598  enq0ref  7616  elnp1st2nd  7659  elrealeu  8012  elreal2  8013  le2tri3i  8251  elnn0nn  9407  elnnnn0b  9409  elnnnn0c  9410  elnnz  9452  elnn0z  9455  elnnz1  9465  elz2  9514  eluz2b2  9794  elnn1uz2  9798  elpqb  9841  elioo4g  10126  eluzfz2b  10225  fzm  10230  elfz1end  10247  fzass4  10254  elfz1b  10282  fz01or  10303  nn0fz0  10311  fzolb  10346  fzom  10357  elfzo0  10378  fzo1fzo0n0  10379  elfzo0z  10380  elfzo1  10386  infssuzex  10448  hash2en  11060  wrdexb  11078  0wrd0  11092  rexanuz  11494  rexuz3  11496  sqrt0rlem  11509  fisum0diag  11947  fprod0diagfz  12134  isprm6  12664  oddpwdclemdc  12690  nnoddn2prmb  12780  4sqlem4  12910  4sqexercise1  12916  ennnfone  12991  ctinfom  12994  ctinf  12996  fnpr2ob  13368  dfgrp2  13555  dfgrp3m  13627  dfgrp3me  13628  isnsg3  13739  invghm  13861  dvdsrzring  14561  zrhval  14575  tgclb  14733  xmetunirn  15026  dich0  15320  elply2  15403  2sqlem2  15788  umgrislfupgrenlem  15922  umgrislfupgrdom  15923  uspgrupgrushgr  15974  usgrumgruspgr  15977  usgruspgrben  15978  usgrislfuspgrdom  15982  bj-nnsn  16055  bdeq  16144  bdop  16196  bdunexb  16241  bj-2inf  16259  bj-nn0suc  16285  nnnninfen  16346  exmidsbth  16351  trirec0  16371  redc0  16384  reap0  16385  cndcap  16386  neap0mkv  16396