Theorem impbii 125

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 118	. 2 ⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → (𝜑 ↔ 𝜓)))
4	1, 2, 3	mp2 16	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bicom  139  biid  170  2th  173  pm5.74  178  bitri  183  bibi2i  226  bi2.04  247  pm5.4  248  imdi  249  impexp  261  ancom  264  pm4.45im  332  dfbi2  385  anass  398  pm5.32  448  jcab  592  notnotnot  623  con2b  658  imnan  679  2false  690  pm5.21nii  693  pm4.8  696  oibabs  703  orcom  717  ioran  741  oridm  746  orbi2i  751  or12  755  pm4.44  768  ordi  805  andi  807  pm4.72  812  stdcndc  830  stdcndcOLD  831  stdcn  832  dcnn  833  pm4.82  934  rnlem  960  3jaob  1280  xoranor  1355  falantru  1381  3impexp  1413  3impexpbicom  1414  alcom  1454  19.26  1457  19.3h  1532  19.3  1533  19.21h  1536  19.43  1607  19.9h  1622  excom  1642  19.41h  1663  19.41  1664  equcom  1682  equsalh  1704  equsex  1706  cbvalh  1726  cbvexh  1728  sbbii  1738  sbh  1749  equs45f  1774  sb6f  1775  sbcof2  1782  sbequ8  1819  sbidm  1823  sb5rf  1824  sb6rf  1825  equvin  1835  sbimv  1865  sbalyz  1972  eu2  2041  eu3h  2042  eu5  2044  mo3h  2050  euan  2053  axext4  2121  cleqh  2237  r19.26  2556  ralcom3  2596  ceqsex  2719  gencbvex  2727  gencbvex2  2728  gencbval  2729  eqvinc  2803  pm13.183  2817  rr19.3v  2818  rr19.28v  2819  reu6  2868  reu3  2869  sbnfc2  3055  difdif  3196  ddifnel  3202  ddifstab  3203  ssddif  3305  difin  3308  uneqin  3322  indifdir  3327  undif3ss  3332  difrab  3345  un00  3404  undifss  3438  ssdifeq0  3440  ralidm  3458  ralf0  3461  ralm  3462  elpr2  3544  snidb  3550  difsnb  3658  preq12b  3692  preqsn  3697  axpweq  4090  exmidn0m  4119  exmidsssn  4120  exmid0el  4122  exmidel  4123  exmidundif  4124  exmidundifim  4125  sspwb  4133  unipw  4134  opm  4151  opth  4154  ssopab2b  4193  elon2  4293  unexb  4358  eusvnfb  4370  eusv2nf  4372  ralxfrALT  4383  uniexb  4389  iunpw  4396  sucelon  4414  unon  4422  sucprcreg  4459  opthreg  4466  ordsuc  4473  dcextest  4490  peano2b  4523  opelxp  4564  opthprc  4585  relop  4684  issetid  4688  xpid11  4757  elres  4850  iss  4860  issref  4916  xpmlem  4954  sqxpeq0  4957  ssrnres  4976  dfrel2  4984  relrelss  5060  fn0  5237  funssxp  5287  f00  5309  f0bi  5310  dffo2  5344  ffoss  5392  f1o00  5395  fo00  5396  fv3  5437  dff2  5557  dffo4  5561  dffo5  5562  fmpt  5563  ffnfv  5571  fsn  5585  fsn2  5587  isores1  5708  ssoprab2b  5821  eqfnov2  5871  cnvoprab  6124  reldmtpos  6143  mapsn  6577  mapsncnv  6582  mptelixpg  6621  elixpsn  6622  ixpsnf1o  6623  en0  6682  en1  6686  dom0  6725  exmidpw  6795  undifdcss  6804  fidcenum  6837  djuexb  6922  ctssdc  6991  exmidomni  7007  exmidfodomr  7053  elni2  7115  ltbtwnnqq  7216  enq0ref  7234  elnp1st2nd  7277  elrealeu  7630  elreal2  7631  le2tri3i  7865  elnn0nn  9012  elnnnn0b  9014  elnnnn0c  9015  elnnz  9057  elnn0z  9060  elnnz1  9070  elz2  9115  eluz2b2  9390  elnn1uz2  9394  elioo4g  9710  eluzfz2b  9806  fzm  9811  elfz1end  9828  fzass4  9835  elfz1b  9863  fz01or  9884  nn0fz0  9892  fzolb  9923  fzom  9934  elfzo0  9952  fzo1fzo0n0  9953  elfzo0z  9954  elfzo1  9960  rexanuz  10753  rexuz3  10755  sqrt0rlem  10768  fisum0diag  11203  infssuzex  11631  isprm6  11814  oddpwdclemdc  11840  ennnfone  11927  ctinfom  11930  ctinf  11932  tgclb  12223  xmetunirn  12516  bj-nnsn  12934  bdeq  13010  bdop  13062  bdunexb  13107  bj-2inf  13125  bj-nn0suc  13151  exmidsbth  13208