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  634  con2b  669  imnan  690  2false  701  pm5.21nii  704  pm4.8  707  oibabs  714  orcom  728  ioran  752  oridm  757  orbi2i  762  or12  766  pm4.44  779  ordi  816  andi  818  pm4.72  827  stdcndc  845  stdcndcOLD  846  stdcn  847  dcnn  848  pm4.82  950  rnlem  976  3jaob  1302  xoranor  1377  falantru  1403  3impexp  1435  3impexpbicom  1436  alcom  1476  19.26  1479  19.3h  1551  19.3  1552  19.21h  1555  19.43  1626  19.9h  1641  excom  1662  19.41h  1683  19.41  1684  equcom  1704  equsalh  1724  equsex  1726  cbvalv1  1749  cbvexv1  1750  cbvalh  1751  cbvexh  1753  sbbii  1763  sbh  1774  equs45f  1800  sb6f  1801  sbcof2  1808  sbequ8  1845  sbidm  1849  sb5rf  1850  sb6rf  1851  equvin  1861  sbimv  1891  cbvalvw  1917  cbvexvw  1918  sbalyz  1997  eu2  2068  eu3h  2069  eu5  2071  mo3h  2077  euan  2080  axext4  2159  cleqh  2275  r19.26  2601  ralcom3  2642  ceqsex  2773  gencbvex  2781  gencbvex2  2782  gencbval  2783  eqvinc  2858  pm13.183  2873  rr19.3v  2874  rr19.28v  2875  reu6  2924  reu3  2925  sbnfc2  3115  difdif  3258  ddifnel  3264  ddifstab  3265  ssddif  3367  difin  3370  uneqin  3384  indifdir  3389  undif3ss  3394  difrab  3407  un00  3467  undifss  3501  ssdifeq0  3503  ralidm  3521  ralf0  3524  ralm  3525  elpr2  3611  snidb  3619  difsnb  3732  preq12b  3766  preqsn  3771  axpweq  4166  exmidn0m  4196  exmidsssn  4197  exmid0el  4199  exmidel  4200  exmidundif  4201  exmidundifim  4202  sspwb  4210  unipw  4211  opm  4228  opth  4231  ssopab2b  4270  elon2  4370  unexb  4436  eusvnfb  4448  eusv2nf  4450  ralxfrALT  4461  uniexb  4467  iunpw  4474  sucelon  4496  unon  4504  sucprcreg  4542  opthreg  4549  ordsuc  4556  dcextest  4574  peano2b  4608  opelxp  4650  opthprc  4671  relop  4770  issetid  4774  xpid11  4843  elres  4936  iss  4946  issref  5003  xpmlem  5041  sqxpeq0  5044  ssrnres  5063  dfrel2  5071  relrelss  5147  fn0  5327  funssxp  5377  f00  5399  f0bi  5400  dffo2  5434  ffoss  5485  f1o00  5488  fo00  5489  fv3  5530  dff2  5652  dffo4  5656  dffo5  5657  fmpt  5658  ffnfv  5666  fsn  5680  fsn2  5682  isores1  5805  ssoprab2b  5922  eqfnov2  5972  cnvoprab  6225  reldmtpos  6244  mapsn  6680  mapsncnv  6685  mptelixpg  6724  elixpsn  6725  ixpsnf1o  6726  en0  6785  en1  6789  dom0  6828  exmidpw  6898  exmidpweq  6899  pw1fin  6900  undifdcss  6912  fidcenum  6945  djuexb  7033  ctssdc  7102  exmidomni  7130  nninfwlpo  7167  exmidfodomr  7193  exmidontri  7228  exmidontri2or  7232  onntri3or  7234  onntri2or  7235  elni2  7288  ltbtwnnqq  7389  enq0ref  7407  elnp1st2nd  7450  elrealeu  7803  elreal2  7804  le2tri3i  8040  elnn0nn  9189  elnnnn0b  9191  elnnnn0c  9192  elnnz  9234  elnn0z  9237  elnnz1  9247  elz2  9295  eluz2b2  9574  elnn1uz2  9578  elpqb  9620  elioo4g  9903  eluzfz2b  10001  fzm  10006  elfz1end  10023  fzass4  10030  elfz1b  10058  fz01or  10079  nn0fz0  10087  fzolb  10121  fzom  10132  elfzo0  10150  fzo1fzo0n0  10151  elfzo0z  10152  elfzo1  10158  rexanuz  10963  rexuz3  10965  sqrt0rlem  10978  fisum0diag  11415  fprod0diagfz  11602  infssuzex  11915  isprm6  12112  oddpwdclemdc  12138  nnoddn2prmb  12227  4sqlem4  12355  ennnfone  12391  ctinfom  12394  ctinf  12396  dfgrp2  12762  dfgrp3m  12828  dfgrp3me  12829  tgclb  13134  xmetunirn  13427  2sqlem2  14020  bj-nnsn  14043  bdeq  14133  bdop  14185  bdunexb  14230  bj-2inf  14248  bj-nn0suc  14274  exmidsbth  14331  trirec0  14351  redc0  14364  reap0  14365