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  697  2false  709  pm5.21nii  712  pm4.8  715  oibabs  722  orcom  736  ioran  760  oridm  765  orbi2i  770  or12  774  pm4.44  787  ordi  824  andi  826  pm4.72  835  stdcndc  853  stdcndcOLD  854  stdcn  855  dcnn  856  pm4.82  959  rnlem  985  3jaob  1339  xoranor  1422  falantru  1448  3impexp  1483  3impexpbicom  1484  alcom  1527  19.26  1530  19.3h  1602  19.3  1603  19.21h  1606  19.43  1677  19.9h  1692  excom  1712  19.41h  1733  19.41  1734  equcom  1754  equsalh  1774  equsex  1776  cbvalv1  1800  cbvexv1  1801  cbvalh  1802  cbvexh  1804  sbbii  1814  sbh  1825  equs45f  1851  sb6f  1852  sbcof2  1859  sbequ8  1896  sbidm  1900  sb5rf  1901  sb6rf  1902  equvin  1912  sbimv  1943  cbvalvw  1969  cbvexvw  1970  sbalyz  2053  eu2  2125  eu3h  2126  eu5  2128  mo3h  2134  euan  2137  axext4  2216  cleqh  2332  r19.26  2669  ralcom3  2711  ceqsex  2852  gencbvex  2861  gencbvex2  2862  gencbval  2863  eqvinc  2940  pm13.183  2955  rr19.3v  2956  rr19.28v  2957  reu6  3006  reu3  3007  sbnfc2  3199  difdif  3344  ddifnel  3350  ddifstab  3351  ssddif  3455  difin  3458  uneqin  3472  indifdir  3477  undif3ss  3482  difrab  3495  un00  3555  undifss  3590  ssdifeq0  3592  ralidm  3610  ralf0  3612  ralm  3613  elpr2  3711  snidb  3719  rabsnifsb  3757  difsnb  3837  preq12b  3874  preqsn  3879  axpweq  4284  exmidn0m  4314  exmidsssn  4315  exmid0el  4317  exmidel  4318  exmidundif  4319  exmidundifim  4320  sspwb  4332  unipw  4333  opm  4350  opth  4353  ssopab2b  4395  elon2  4497  unexb  4563  eusvnfb  4575  eusv2nf  4577  ralxfrALT  4588  uniexb  4594  iunpw  4601  onsucb  4625  unon  4633  sucprcreg  4671  opthreg  4678  ordsuc  4685  dcextest  4703  peano2b  4737  opelxp  4779  opthprc  4801  relop  4905  issetid  4909  xpid11  4980  elres  5074  iss  5084  issref  5145  xpmlem  5183  sqxpeq0  5186  ssrnres  5205  dfrel2  5213  relrelss  5289  fn0  5478  funssxp  5532  f00  5559  f0bi  5560  dffo2  5594  ffoss  5647  f1o00  5651  fo00  5652  fv3  5693  dff2  5821  dffo4  5825  dffo5  5826  fmpt  5827  ffnfv  5835  fsn  5849  fsn2  5851  funop  5861  isores1  5987  ssoprab2b  6110  eqfnov2  6161  cnvoprab  6430  reldmtpos  6484  mapsn  6925  mapsncnv  6930  mptelixpg  6969  elixpsn  6970  ixpsnf1o  6971  en0  7035  en1  7039  modom  7061  dom0  7091  exmidpw  7168  exmidpweq  7169  pw1fin  7170  exmidpw2en  7172  undifdcss  7183  exmidssfi  7199  residfi  7207  fidcenum  7226  djuexb  7335  ctssdc  7404  exmidomni  7433  nninfinfwlpo  7471  nninfwlpo  7472  exmidfodomr  7507  iftrueb01  7533  exmidontri  7549  exmidontri2or  7553  onntri3or  7555  onntri2or  7556  dftap2  7565  exmidmotap  7575  elni2  7629  ltbtwnnqq  7730  enq0ref  7748  elnp1st2nd  7791  elrealeu  8144  elreal2  8145  le2tri3i  8382  elnn0nn  9538  elnnnn0b  9540  elnnnn0c  9541  elnnz  9587  elnn0z  9590  elnnz1  9600  elz2  9649  eluz2b2  9935  elnn1uz2  9939  elpqb  9982  elioo4g  10267  eluzfz2b  10367  fzm  10372  elfz1end  10389  fzass4  10396  elfz1b  10424  fz01or  10445  nn0fz0  10453  fzolb  10488  fzom  10499  elfzo0  10520  fzo1fzo0n0  10522  elfzo0z  10523  elfzo1  10530  infssuzex  10593  hash2en  11215  wrdexb  11236  0wrd0  11250  rexanuz  11673  rexuz3  11675  sqrt0rlem  11688  fisum0diag  12127  fprod0diagfz  12314  isprm6  12844  oddpwdclemdc  12870  nnoddn2prmb  12960  4sqlem4  13090  4sqexercise1  13096  ballotfilem2  13142  ennnfone  13176  ctinfom  13179  ctinf  13181  fnpr2ob  13553  dfgrp2  13740  dfgrp3m  13812  dfgrp3me  13813  isnsg3  13924  invghm  14046  dvdsrzring  14751  zrhval  14765  tgclb  14930  xmetunirn  15223  dich0  15517  elply2  15600  2sqlem2  15988  umgrislfupgrenlem  16125  umgrislfupgrdom  16126  uspgrupgrushgr  16177  usgrumgruspgr  16180  usgruspgrben  16181  usgrislfuspgrdom  16185  clwwlkn1loopb  16415  bj-nnsn  16505  bdeq  16593  bdop  16645  bdunexb  16690  bj-2inf  16708  bj-nn0suc  16734  pw1dceq  16778  exmidnotnotr  16779  exmidcon  16780  exmidpeirce  16781  nnnninfen  16799  exmidsbth  16804  trirec0  16828  redc0  16842  reap0  16843  cndcap  16844  neap0mkv  16855