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  696  2false  708  pm5.21nii  711  pm4.8  714  oibabs  721  orcom  735  ioran  759  oridm  764  orbi2i  769  or12  773  pm4.44  786  ordi  823  andi  825  pm4.72  834  stdcndc  852  stdcndcOLD  853  stdcn  854  dcnn  855  pm4.82  958  rnlem  984  3jaob  1338  xoranor  1421  falantru  1447  3impexp  1482  3impexpbicom  1483  alcom  1526  19.26  1529  19.3h  1601  19.3  1602  19.21h  1605  19.43  1676  19.9h  1691  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  2659  ralcom3  2701  ceqsex  2841  gencbvex  2850  gencbvex2  2851  gencbval  2852  eqvinc  2929  pm13.183  2944  rr19.3v  2945  rr19.28v  2946  reu6  2995  reu3  2996  sbnfc2  3188  difdif  3332  ddifnel  3338  ddifstab  3339  ssddif  3441  difin  3444  uneqin  3458  indifdir  3463  undif3ss  3468  difrab  3481  un00  3541  undifss  3575  ssdifeq0  3577  ralidm  3595  ralf0  3597  ralm  3598  elpr2  3691  snidb  3699  rabsnifsb  3737  difsnb  3816  preq12b  3853  preqsn  3858  axpweq  4261  exmidn0m  4291  exmidsssn  4292  exmid0el  4294  exmidel  4295  exmidundif  4296  exmidundifim  4297  sspwb  4308  unipw  4309  opm  4326  opth  4329  ssopab2b  4371  elon2  4473  unexb  4539  eusvnfb  4551  eusv2nf  4553  ralxfrALT  4564  uniexb  4570  iunpw  4577  onsucb  4601  unon  4609  sucprcreg  4647  opthreg  4654  ordsuc  4661  dcextest  4679  peano2b  4713  opelxp  4755  opthprc  4777  relop  4880  issetid  4884  xpid11  4955  elres  5049  iss  5059  issref  5119  xpmlem  5157  sqxpeq0  5160  ssrnres  5179  dfrel2  5187  relrelss  5263  fn0  5452  funssxp  5504  f00  5528  f0bi  5529  dffo2  5563  ffoss  5616  f1o00  5620  fo00  5621  fv3  5662  dff2  5791  dffo4  5795  dffo5  5796  fmpt  5797  ffnfv  5805  fsn  5819  fsn2  5821  funop  5830  isores1  5954  ssoprab2b  6077  eqfnov2  6128  cnvoprab  6398  reldmtpos  6418  mapsn  6858  mapsncnv  6863  mptelixpg  6902  elixpsn  6903  ixpsnf1o  6904  en0  6968  en1  6972  modom  6993  dom0  7023  exmidpw  7099  exmidpweq  7100  pw1fin  7101  exmidpw2en  7103  undifdcss  7114  exmidssfi  7130  residfi  7138  fidcenum  7154  djuexb  7242  ctssdc  7311  exmidomni  7340  nninfinfwlpo  7378  nninfwlpo  7379  exmidfodomr  7414  iftrueb01  7440  exmidontri  7456  exmidontri2or  7460  onntri3or  7462  onntri2or  7463  dftap2  7469  exmidmotap  7479  elni2  7533  ltbtwnnqq  7634  enq0ref  7652  elnp1st2nd  7695  elrealeu  8048  elreal2  8049  le2tri3i  8287  elnn0nn  9443  elnnnn0b  9445  elnnnn0c  9446  elnnz  9488  elnn0z  9491  elnnz1  9501  elz2  9550  eluz2b2  9836  elnn1uz2  9840  elpqb  9883  elioo4g  10168  eluzfz2b  10267  fzm  10272  elfz1end  10289  fzass4  10296  elfz1b  10324  fz01or  10345  nn0fz0  10353  fzolb  10388  fzom  10399  elfzo0  10420  fzo1fzo0n0  10421  elfzo0z  10422  elfzo1  10429  infssuzex  10492  hash2en  11106  wrdexb  11124  0wrd0  11138  rexanuz  11548  rexuz3  11550  sqrt0rlem  11563  fisum0diag  12001  fprod0diagfz  12188  isprm6  12718  oddpwdclemdc  12744  nnoddn2prmb  12834  4sqlem4  12964  4sqexercise1  12970  ennnfone  13045  ctinfom  13048  ctinf  13050  fnpr2ob  13422  dfgrp2  13609  dfgrp3m  13681  dfgrp3me  13682  isnsg3  13793  invghm  13915  dvdsrzring  14616  zrhval  14630  tgclb  14788  xmetunirn  15081  dich0  15375  elply2  15458  2sqlem2  15843  umgrislfupgrenlem  15980  umgrislfupgrdom  15981  uspgrupgrushgr  16032  usgrumgruspgr  16035  usgruspgrben  16036  usgrislfuspgrdom  16040  clwwlkn1loopb  16270  bj-nnsn  16329  bdeq  16418  bdop  16470  bdunexb  16515  bj-2inf  16533  bj-nn0suc  16559  pw1dceq  16605  nnnninfen  16623  exmidsbth  16628  trirec0  16648  redc0  16661  reap0  16662  cndcap  16663  neap0mkv  16673