Theorem impbii 124

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

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bicom  138  biid  169  2th  172  pm5.74  177  bitri  182  bibi2i  225  bi2.04  246  pm5.4  247  imdi  248  impexp  259  ancom  262  pm4.45im  327  dfbi2  380  anass  393  pm5.32  441  jcab  568  con2b  626  2false  650  pm5.21nii  653  pm4.8  656  imnan  657  notnotnot  661  orcom  680  ioran  702  oridm  707  orbi2i  712  or12  716  pm4.44  729  ordi  763  andi  765  pm4.72  770  oibabs  836  stabtestimpdc  860  pm4.82  894  rnlem  920  3jaob  1236  xoranor  1311  falantru  1337  3impexp  1369  3impexpbicom  1370  alcom  1410  19.26  1413  19.3h  1488  19.3  1489  19.21h  1492  19.43  1562  19.9h  1577  excom  1597  19.41h  1618  19.41  1619  equcom  1637  equsalh  1658  equsex  1660  cbvalh  1680  cbvexh  1682  sbbii  1692  sbh  1703  equs45f  1727  sb6f  1728  sbcof2  1735  sbequ8  1772  sbidm  1776  sb5rf  1777  sb6rf  1778  equvin  1788  sbimv  1818  sbalyz  1920  eu2  1989  eu3h  1990  eu5  1992  mo3h  1998  euan  2001  axext4  2069  cleqh  2184  r19.26  2493  ralcom3  2530  ceqsex  2651  gencbvex  2659  gencbvex2  2660  gencbval  2661  eqvinc  2731  pm13.183  2745  rr19.3v  2746  rr19.28v  2747  reu6  2795  reu3  2796  sbnfc2  2977  difdif  3114  ddifnel  3120  ddifstab  3121  ssddif  3222  difin  3225  uneqin  3239  indifdir  3244  undif3ss  3249  difrab  3262  un00  3317  undifss  3350  ssdifeq0  3352  ralidm  3369  ralf0  3372  ralm  3373  elpr2  3453  snidb  3457  difsnb  3563  preq12b  3597  preqsn  3602  axpweq  3980  exmid0el  4006  exmidel  4007  exmidundif  4008  sspwb  4016  unipw  4017  opm  4034  opth  4037  ssopab2b  4076  elon2  4176  unexb  4240  eusvnfb  4249  eusv2nf  4251  ralxfrALT  4262  uniexb  4268  iunpw  4274  sucelon  4292  unon  4300  sucprcreg  4337  opthreg  4344  ordsuc  4351  dcextest  4368  peano2b  4401  opelxp  4439  opthprc  4456  relop  4553  issetid  4557  elres  4714  iss  4724  issref  4778  xpmlem  4815  ssrnres  4836  dfrel2  4844  relrelss  4920  fn0  5095  funssxp  5138  f00  5159  f0bi  5160  dffo2  5194  ffoss  5242  f1o00  5245  fo00  5246  fv3  5285  dff2  5400  dffo4  5404  dffo5  5405  fmpt  5406  ffnfv  5413  fsn  5426  fsn2  5428  isores1  5548  ssoprab2b  5657  eqfnov2  5703  cnvoprab  5950  reldmtpos  5966  mapsn  6393  mapsncnv  6398  en0  6458  en1  6462  dom0  6500  exmidpw  6570  undifdcss  6579  exmidomni  6735  exmidfodomr  6767  elni2  6810  ltbtwnnqq  6911  enq0ref  6929  elnp1st2nd  6972  elrealeu  7304  elreal2  7305  le2tri3i  7530  elnn0nn  8641  elnnnn0b  8643  elnnnn0c  8644  elnnz  8686  elnn0z  8689  elnnz1  8699  elz2  8744  eluz2b2  9015  elnn1uz2  9019  elioo4g  9277  eluzfz2b  9372  fzm  9377  elfz1end  9394  fzass4  9400  elfz1b  9427  fz01or  9448  nn0fz0  9454  fzolb  9485  fzom  9496  elfzo0  9514  fzo1fzo0n0  9515  elfzo0z  9516  elfzo1  9522  rexanuz  10309  rexuz3  10311  sqrt0rlem  10324  infssuzex  10812  isprm6  10993  oddpwdclemdc  11018  bdeq  11144  bdop  11196  bdunexb  11241  bj-2inf  11263  bj-nn0suc  11289  exmidsbth  11344