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  2839  gencbvex  2848  gencbvex2  2849  gencbval  2850  eqvinc  2927  pm13.183  2942  rr19.3v  2943  rr19.28v  2944  reu6  2993  reu3  2994  sbnfc2  3186  difdif  3330  ddifnel  3336  ddifstab  3337  ssddif  3439  difin  3442  uneqin  3456  indifdir  3461  undif3ss  3466  difrab  3479  un00  3539  undifss  3573  ssdifeq0  3575  ralidm  3593  ralf0  3595  ralm  3596  elpr2  3689  snidb  3697  rabsnifsb  3735  difsnb  3814  preq12b  3851  preqsn  3856  axpweq  4259  exmidn0m  4289  exmidsssn  4290  exmid0el  4292  exmidel  4293  exmidundif  4294  exmidundifim  4295  sspwb  4306  unipw  4307  opm  4324  opth  4327  ssopab2b  4369  elon2  4471  unexb  4537  eusvnfb  4549  eusv2nf  4551  ralxfrALT  4562  uniexb  4568  iunpw  4575  onsucb  4599  unon  4607  sucprcreg  4645  opthreg  4652  ordsuc  4659  dcextest  4677  peano2b  4711  opelxp  4753  opthprc  4775  relop  4878  issetid  4882  xpid11  4953  elres  5047  iss  5057  issref  5117  xpmlem  5155  sqxpeq0  5158  ssrnres  5177  dfrel2  5185  relrelss  5261  fn0  5449  funssxp  5501  f00  5525  f0bi  5526  dffo2  5560  ffoss  5612  f1o00  5616  fo00  5617  fv3  5658  dff2  5787  dffo4  5791  dffo5  5792  fmpt  5793  ffnfv  5801  fsn  5815  fsn2  5817  funop  5826  isores1  5950  ssoprab2b  6073  eqfnov2  6124  cnvoprab  6394  reldmtpos  6414  mapsn  6854  mapsncnv  6859  mptelixpg  6898  elixpsn  6899  ixpsnf1o  6900  en0  6964  en1  6968  modom  6989  dom0  7019  exmidpw  7093  exmidpweq  7094  pw1fin  7095  exmidpw2en  7097  undifdcss  7108  residfi  7130  fidcenum  7146  djuexb  7234  ctssdc  7303  exmidomni  7332  nninfinfwlpo  7370  nninfwlpo  7371  exmidfodomr  7405  iftrueb01  7431  exmidontri  7447  exmidontri2or  7451  onntri3or  7453  onntri2or  7454  dftap2  7460  exmidmotap  7470  elni2  7524  ltbtwnnqq  7625  enq0ref  7643  elnp1st2nd  7686  elrealeu  8039  elreal2  8040  le2tri3i  8278  elnn0nn  9434  elnnnn0b  9436  elnnnn0c  9437  elnnz  9479  elnn0z  9482  elnnz1  9492  elz2  9541  eluz2b2  9827  elnn1uz2  9831  elpqb  9874  elioo4g  10159  eluzfz2b  10258  fzm  10263  elfz1end  10280  fzass4  10287  elfz1b  10315  fz01or  10336  nn0fz0  10344  fzolb  10379  fzom  10390  elfzo0  10411  fzo1fzo0n0  10412  elfzo0z  10413  elfzo1  10420  infssuzex  10483  hash2en  11097  wrdexb  11115  0wrd0  11129  rexanuz  11539  rexuz3  11541  sqrt0rlem  11554  fisum0diag  11992  fprod0diagfz  12179  isprm6  12709  oddpwdclemdc  12735  nnoddn2prmb  12825  4sqlem4  12955  4sqexercise1  12961  ennnfone  13036  ctinfom  13039  ctinf  13041  fnpr2ob  13413  dfgrp2  13600  dfgrp3m  13672  dfgrp3me  13673  isnsg3  13784  invghm  13906  dvdsrzring  14607  zrhval  14621  tgclb  14779  xmetunirn  15072  dich0  15366  elply2  15449  2sqlem2  15834  umgrislfupgrenlem  15969  umgrislfupgrdom  15970  uspgrupgrushgr  16021  usgrumgruspgr  16024  usgruspgrben  16025  usgrislfuspgrdom  16029  clwwlkn1loopb  16215  bj-nnsn  16265  bdeq  16354  bdop  16406  bdunexb  16451  bj-2inf  16469  bj-nn0suc  16495  pw1dceq  16541  nnnninfen  16559  exmidsbth  16564  trirec0  16584  redc0  16597  reap0  16598  cndcap  16599  neap0mkv  16609