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  1314  xoranor  1396  falantru  1422  3impexp  1456  3impexpbicom  1457  alcom  1500  19.26  1503  19.3h  1575  19.3  1576  19.21h  1579  19.43  1650  19.9h  1665  excom  1686  19.41h  1707  19.41  1708  equcom  1728  equsalh  1748  equsex  1750  cbvalv1  1773  cbvexv1  1774  cbvalh  1775  cbvexh  1777  sbbii  1787  sbh  1798  equs45f  1824  sb6f  1825  sbcof2  1832  sbequ8  1869  sbidm  1873  sb5rf  1874  sb6rf  1875  equvin  1885  sbimv  1916  cbvalvw  1942  cbvexvw  1943  sbalyz  2026  eu2  2097  eu3h  2098  eu5  2100  mo3h  2106  euan  2109  axext4  2188  cleqh  2304  r19.26  2631  ralcom3  2673  ceqsex  2809  gencbvex  2818  gencbvex2  2819  gencbval  2820  eqvinc  2895  pm13.183  2910  rr19.3v  2911  rr19.28v  2912  reu6  2961  reu3  2962  sbnfc2  3153  difdif  3297  ddifnel  3303  ddifstab  3304  ssddif  3406  difin  3409  uneqin  3423  indifdir  3428  undif3ss  3433  difrab  3446  un00  3506  undifss  3540  ssdifeq0  3542  ralidm  3560  ralf0  3562  ralm  3563  elpr2  3654  snidb  3662  difsnb  3775  preq12b  3810  preqsn  3815  axpweq  4214  exmidn0m  4244  exmidsssn  4245  exmid0el  4247  exmidel  4248  exmidundif  4249  exmidundifim  4250  sspwb  4259  unipw  4260  opm  4277  opth  4280  ssopab2b  4321  elon2  4421  unexb  4487  eusvnfb  4499  eusv2nf  4501  ralxfrALT  4512  uniexb  4518  iunpw  4525  onsucb  4549  unon  4557  sucprcreg  4595  opthreg  4602  ordsuc  4609  dcextest  4627  peano2b  4661  opelxp  4703  opthprc  4724  relop  4826  issetid  4830  xpid11  4899  elres  4992  iss  5002  issref  5062  xpmlem  5100  sqxpeq0  5103  ssrnres  5122  dfrel2  5130  relrelss  5206  fn0  5389  funssxp  5439  f00  5461  f0bi  5462  dffo2  5496  ffoss  5548  f1o00  5551  fo00  5552  fv3  5593  dff2  5718  dffo4  5722  dffo5  5723  fmpt  5724  ffnfv  5732  fsn  5746  fsn2  5748  isores1  5873  ssoprab2b  5992  eqfnov2  6043  cnvoprab  6310  reldmtpos  6329  mapsn  6767  mapsncnv  6772  mptelixpg  6811  elixpsn  6812  ixpsnf1o  6813  en0  6872  en1  6876  dom0  6917  exmidpw  6987  exmidpweq  6988  pw1fin  6989  exmidpw2en  6991  undifdcss  7002  residfi  7024  fidcenum  7040  djuexb  7128  ctssdc  7197  exmidomni  7226  nninfinfwlpo  7264  nninfwlpo  7265  exmidfodomr  7294  exmidontri  7333  exmidontri2or  7337  onntri3or  7339  onntri2or  7340  dftap2  7345  exmidmotap  7355  elni2  7409  ltbtwnnqq  7510  enq0ref  7528  elnp1st2nd  7571  elrealeu  7924  elreal2  7925  le2tri3i  8163  elnn0nn  9319  elnnnn0b  9321  elnnnn0c  9322  elnnz  9364  elnn0z  9367  elnnz1  9377  elz2  9426  eluz2b2  9706  elnn1uz2  9710  elpqb  9753  elioo4g  10038  eluzfz2b  10137  fzm  10142  elfz1end  10159  fzass4  10166  elfz1b  10194  fz01or  10215  nn0fz0  10223  fzolb  10258  fzom  10269  elfzo0  10287  fzo1fzo0n0  10288  elfzo0z  10289  elfzo1  10295  infssuzex  10357  wrdexb  10981  0wrd0  10995  rexanuz  11218  rexuz3  11220  sqrt0rlem  11233  fisum0diag  11671  fprod0diagfz  11858  isprm6  12388  oddpwdclemdc  12414  nnoddn2prmb  12504  4sqlem4  12634  4sqexercise1  12640  ennnfone  12715  ctinfom  12718  ctinf  12720  fnpr2ob  13090  dfgrp2  13277  dfgrp3m  13349  dfgrp3me  13350  isnsg3  13461  invghm  13583  dvdsrzring  14283  zrhval  14297  tgclb  14455  xmetunirn  14748  dich0  15042  elply2  15125  2sqlem2  15510  bj-nnsn  15533  bdeq  15623  bdop  15675  bdunexb  15720  bj-2inf  15738  bj-nn0suc  15764  nnnninfen  15822  exmidsbth  15827  trirec0  15847  redc0  15860  reap0  15861  cndcap  15862  neap0mkv  15872