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  1489  19.26  1492  19.3h  1564  19.3  1565  19.21h  1568  19.43  1639  19.9h  1654  excom  1675  19.41h  1696  19.41  1697  equcom  1717  equsalh  1737  equsex  1739  cbvalv1  1762  cbvexv1  1763  cbvalh  1764  cbvexh  1766  sbbii  1776  sbh  1787  equs45f  1813  sb6f  1814  sbcof2  1821  sbequ8  1858  sbidm  1862  sb5rf  1863  sb6rf  1864  equvin  1874  sbimv  1905  cbvalvw  1931  cbvexvw  1932  sbalyz  2015  eu2  2086  eu3h  2087  eu5  2089  mo3h  2095  euan  2098  axext4  2177  cleqh  2293  r19.26  2620  ralcom3  2662  ceqsex  2798  gencbvex  2806  gencbvex2  2807  gencbval  2808  eqvinc  2883  pm13.183  2898  rr19.3v  2899  rr19.28v  2900  reu6  2949  reu3  2950  sbnfc2  3141  difdif  3284  ddifnel  3290  ddifstab  3291  ssddif  3393  difin  3396  uneqin  3410  indifdir  3415  undif3ss  3420  difrab  3433  un00  3493  undifss  3527  ssdifeq0  3529  ralidm  3547  ralf0  3549  ralm  3550  elpr2  3640  snidb  3648  difsnb  3761  preq12b  3796  preqsn  3801  axpweq  4200  exmidn0m  4230  exmidsssn  4231  exmid0el  4233  exmidel  4234  exmidundif  4235  exmidundifim  4236  sspwb  4245  unipw  4246  opm  4263  opth  4266  ssopab2b  4307  elon2  4407  unexb  4473  eusvnfb  4485  eusv2nf  4487  ralxfrALT  4498  uniexb  4504  iunpw  4511  onsucb  4535  unon  4543  sucprcreg  4581  opthreg  4588  ordsuc  4595  dcextest  4613  peano2b  4647  opelxp  4689  opthprc  4710  relop  4812  issetid  4816  xpid11  4885  elres  4978  iss  4988  issref  5048  xpmlem  5086  sqxpeq0  5089  ssrnres  5108  dfrel2  5116  relrelss  5192  fn0  5373  funssxp  5423  f00  5445  f0bi  5446  dffo2  5480  ffoss  5532  f1o00  5535  fo00  5536  fv3  5577  dff2  5702  dffo4  5706  dffo5  5707  fmpt  5708  ffnfv  5716  fsn  5730  fsn2  5732  isores1  5857  ssoprab2b  5975  eqfnov2  6026  cnvoprab  6287  reldmtpos  6306  mapsn  6744  mapsncnv  6749  mptelixpg  6788  elixpsn  6789  ixpsnf1o  6790  en0  6849  en1  6853  dom0  6894  exmidpw  6964  exmidpweq  6965  pw1fin  6966  exmidpw2en  6968  undifdcss  6979  residfi  6999  fidcenum  7015  djuexb  7103  ctssdc  7172  exmidomni  7201  nninfwlpo  7238  exmidfodomr  7264  exmidontri  7299  exmidontri2or  7303  onntri3or  7305  onntri2or  7306  dftap2  7311  exmidmotap  7321  elni2  7374  ltbtwnnqq  7475  enq0ref  7493  elnp1st2nd  7536  elrealeu  7889  elreal2  7890  le2tri3i  8128  elnn0nn  9282  elnnnn0b  9284  elnnnn0c  9285  elnnz  9327  elnn0z  9330  elnnz1  9340  elz2  9388  eluz2b2  9668  elnn1uz2  9672  elpqb  9715  elioo4g  10000  eluzfz2b  10099  fzm  10104  elfz1end  10121  fzass4  10128  elfz1b  10156  fz01or  10177  nn0fz0  10185  fzolb  10220  fzom  10231  elfzo0  10249  fzo1fzo0n0  10250  elfzo0z  10251  elfzo1  10257  wrdexb  10926  0wrd0  10940  rexanuz  11132  rexuz3  11134  sqrt0rlem  11147  fisum0diag  11584  fprod0diagfz  11771  infssuzex  12086  isprm6  12285  oddpwdclemdc  12311  nnoddn2prmb  12400  4sqlem4  12530  4sqexercise1  12536  ennnfone  12582  ctinfom  12585  ctinf  12587  fnpr2ob  12923  dfgrp2  13099  dfgrp3m  13171  dfgrp3me  13172  isnsg3  13277  invghm  13399  dvdsrzring  14091  zrhval  14105  tgclb  14233  xmetunirn  14526  dich0  14806  elply2  14881  2sqlem2  15202  bj-nnsn  15225  bdeq  15315  bdop  15367  bdunexb  15412  bj-2inf  15430  bj-nn0suc  15456  nnnninfen  15511  exmidsbth  15514  trirec0  15534  redc0  15547  reap0  15548  cndcap  15549  neap0mkv  15559