Theorem impbii 117

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

Syntax hints:   → wi 4   ↔ wb 98

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  bicom  128  biid  160  2th  163  pm5.74  168  bitri  173  bibi2i  216  bi2.04  237  pm5.4  238  imdi  239  impexp  250  ancom  253  pm4.45im  317  dfbi2  368  anass  381  pm5.32  426  jcab  535  con2b  593  2false  617  pm5.21nii  620  pm4.8  623  imnan  624  notnotnot  628  orcom  647  ioran  669  oridm  674  orbi2i  679  or12  683  pm4.44  696  ordi  729  andi  731  pm4.72  736  oibabs  800  stabtestimpdc  824  pm4.82  857  rnlem  883  3jaob  1197  truanOLD  1261  xoranor  1268  falantru  1294  3impexp  1326  3impexpbicom  1327  alcom  1367  19.26  1370  19.3h  1445  19.3  1446  19.21h  1449  19.43  1519  19.9h  1534  excom  1554  19.41h  1575  19.41  1576  equcom  1593  equsalh  1614  equsex  1616  cbvalh  1636  cbvexh  1638  sbbii  1648  sbh  1659  equs45f  1683  sb6f  1684  sbcof2  1691  sbequ8  1727  sbidm  1731  sb5rf  1732  sb6rf  1733  equvin  1743  sbimv  1773  sbalyz  1875  eu2  1944  eu3h  1945  eu5  1947  mo3h  1953  euan  1956  axext4  2024  cleqh  2137  r19.26  2441  ralcom3  2477  ceqsex  2592  gencbvex  2600  gencbvex2  2601  gencbval  2602  eqvinc  2667  pm13.183  2681  rr19.3v  2682  rr19.28v  2683  reu6  2730  reu3  2731  sbnfc2  2906  difdif  3069  ddifnel  3075  ssddif  3171  difin  3174  uneqin  3188  indifdir  3193  undif3ss  3198  difrab  3211  un00  3263  undifss  3303  ssdifeq0  3305  ralidm  3321  ralf0  3324  ralm  3325  elpr2  3397  snidb  3401  difsnb  3506  preq12b  3541  preqsn  3546  axpweq  3924  sspwb  3952  unipw  3953  opm  3971  opth  3974  ssopab2b  4013  elon2  4113  unexb  4177  eusvnfb  4186  eusv2nf  4188  ralxfrALT  4199  uniexb  4205  iunpw  4211  sucelon  4229  unon  4237  sucprcreg  4273  opthreg  4280  ordsuc  4287  peano2b  4337  opelxp  4374  opthprc  4391  relop  4486  issetid  4490  elres  4646  iss  4654  issref  4707  xpmlem  4744  ssrnres  4763  dfrel2  4771  relrelss  4844  fn0  5018  funssxp  5060  f00  5081  dffo2  5110  ffoss  5158  f1o00  5161  fo00  5162  fv3  5197  dff2  5311  dffo4  5315  dffo5  5316  fmpt  5319  ffnfv  5323  fsn  5335  fsn2  5337  isores1  5454  ssoprab2b  5562  eqfnov2  5608  reldmtpos  5868  en0  6275  en1  6279  elni2  6412  ltbtwnnqq  6513  enq0ref  6531  elnp1st2nd  6574  elrealeu  6906  elreal2  6907  le2tri3i  7126  elnn0nn  8224  elnnnn0b  8226  elnnnn0c  8227  elnnz  8255  elnn0z  8258  elnnz1  8268  elz2  8312  eluz2b2  8540  elnn1uz2  8544  elioo4g  8803  eluzfz2b  8897  fzm  8902  elfz1end  8919  fzass4  8925  elfz1b  8952  nn0fz0  8978  fzolb  9009  fzom  9020  elfzo0  9038  fzo1fzo0n0  9039  elfzo0z  9040  elfzo1  9046  rexanuz  9587  rexuz3  9588  sqrt0rlem  9601  bdeq  9943  bdop  9995  bdunexb  10040  bj-2inf  10062  bj-nn0suc  10089