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  1799  cbvexv1  1800  cbvalh  1801  cbvexh  1803  sbbii  1813  sbh  1824  equs45f  1850  sb6f  1851  sbcof2  1858  sbequ8  1895  sbidm  1899  sb5rf  1900  sb6rf  1901  equvin  1911  sbimv  1942  cbvalvw  1968  cbvexvw  1969  sbalyz  2052  eu2  2124  eu3h  2125  eu5  2127  mo3h  2133  euan  2136  axext4  2215  cleqh  2331  r19.26  2660  ralcom3  2702  ceqsex  2842  gencbvex  2851  gencbvex2  2852  gencbval  2853  eqvinc  2930  pm13.183  2945  rr19.3v  2946  rr19.28v  2947  reu6  2996  reu3  2997  sbnfc2  3189  difdif  3334  ddifnel  3340  ddifstab  3341  ssddif  3443  difin  3446  uneqin  3460  indifdir  3465  undif3ss  3470  difrab  3483  un00  3543  undifss  3577  ssdifeq0  3579  ralidm  3597  ralf0  3599  ralm  3600  elpr2  3695  snidb  3703  rabsnifsb  3741  difsnb  3821  preq12b  3858  preqsn  3863  axpweq  4267  exmidn0m  4297  exmidsssn  4298  exmid0el  4300  exmidel  4301  exmidundif  4302  exmidundifim  4303  sspwb  4314  unipw  4315  opm  4332  opth  4335  ssopab2b  4377  elon2  4479  unexb  4545  eusvnfb  4557  eusv2nf  4559  ralxfrALT  4570  uniexb  4576  iunpw  4583  onsucb  4607  unon  4615  sucprcreg  4653  opthreg  4660  ordsuc  4667  dcextest  4685  peano2b  4719  opelxp  4761  opthprc  4783  relop  4886  issetid  4890  xpid11  4961  elres  5055  iss  5065  issref  5126  xpmlem  5164  sqxpeq0  5167  ssrnres  5186  dfrel2  5194  relrelss  5270  fn0  5459  funssxp  5512  f00  5537  f0bi  5538  dffo2  5572  ffoss  5625  f1o00  5629  fo00  5630  fv3  5671  dff2  5799  dffo4  5803  dffo5  5804  fmpt  5805  ffnfv  5813  fsn  5827  fsn2  5829  funop  5839  isores1  5965  ssoprab2b  6088  eqfnov2  6139  cnvoprab  6408  reldmtpos  6462  mapsn  6902  mapsncnv  6907  mptelixpg  6946  elixpsn  6947  ixpsnf1o  6948  en0  7012  en1  7016  modom  7037  dom0  7067  exmidpw  7143  exmidpweq  7144  pw1fin  7145  exmidpw2en  7147  undifdcss  7158  exmidssfi  7174  residfi  7182  fidcenum  7198  djuexb  7286  ctssdc  7355  exmidomni  7384  nninfinfwlpo  7422  nninfwlpo  7423  exmidfodomr  7458  iftrueb01  7484  exmidontri  7500  exmidontri2or  7504  onntri3or  7506  onntri2or  7507  dftap2  7513  exmidmotap  7523  elni2  7577  ltbtwnnqq  7678  enq0ref  7696  elnp1st2nd  7739  elrealeu  8092  elreal2  8093  le2tri3i  8330  elnn0nn  9486  elnnnn0b  9488  elnnnn0c  9489  elnnz  9533  elnn0z  9536  elnnz1  9546  elz2  9595  eluz2b2  9881  elnn1uz2  9885  elpqb  9928  elioo4g  10213  eluzfz2b  10313  fzm  10318  elfz1end  10335  fzass4  10342  elfz1b  10370  fz01or  10391  nn0fz0  10399  fzolb  10434  fzom  10445  elfzo0  10466  fzo1fzo0n0  10468  elfzo0z  10469  elfzo1  10476  infssuzex  10539  hash2en  11153  wrdexb  11174  0wrd0  11188  rexanuz  11611  rexuz3  11613  sqrt0rlem  11626  fisum0diag  12065  fprod0diagfz  12252  isprm6  12782  oddpwdclemdc  12808  nnoddn2prmb  12898  4sqlem4  13028  4sqexercise1  13034  ennnfone  13109  ctinfom  13112  ctinf  13114  fnpr2ob  13486  dfgrp2  13673  dfgrp3m  13745  dfgrp3me  13746  isnsg3  13857  invghm  13979  dvdsrzring  14682  zrhval  14696  tgclb  14859  xmetunirn  15152  dich0  15446  elply2  15529  2sqlem2  15917  umgrislfupgrenlem  16054  umgrislfupgrdom  16055  uspgrupgrushgr  16106  usgrumgruspgr  16109  usgruspgrben  16110  usgrislfuspgrdom  16114  clwwlkn1loopb  16344  bj-nnsn  16434  bdeq  16522  bdop  16574  bdunexb  16619  bj-2inf  16637  bj-nn0suc  16663  pw1dceq  16709  exmidnotnotr  16710  exmidcon  16711  exmidpeirce  16712  nnnninfen  16730  exmidsbth  16735  trirec0  16759  redc0  16773  reap0  16774  cndcap  16775  neap0mkv  16785