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  440  jcab  567  con2b  625  2false  649  pm5.21nii  652  pm4.8  655  imnan  656  notnotnot  660  orcom  679  ioran  701  oridm  706  orbi2i  711  or12  715  pm4.44  728  ordi  762  andi  764  pm4.72  769  oibabs  833  stabtestimpdc  857  pm4.82  891  rnlem  917  3jaob  1233  xoranor  1308  falantru  1334  3impexp  1366  3impexpbicom  1367  alcom  1407  19.26  1410  19.3h  1485  19.3  1486  19.21h  1489  19.43  1559  19.9h  1574  excom  1594  19.41h  1615  19.41  1616  equcom  1633  equsalh  1654  equsex  1656  cbvalh  1676  cbvexh  1678  sbbii  1688  sbh  1699  equs45f  1723  sb6f  1724  sbcof2  1731  sbequ8  1768  sbidm  1772  sb5rf  1773  sb6rf  1774  equvin  1784  sbimv  1814  sbalyz  1916  eu2  1985  eu3h  1986  eu5  1988  mo3h  1994  euan  1997  axext4  2065  cleqh  2178  r19.26  2485  ralcom3  2521  ceqsex  2637  gencbvex  2645  gencbvex2  2646  gencbval  2647  eqvinc  2718  pm13.183  2732  rr19.3v  2733  rr19.28v  2734  reu6  2781  reu3  2782  sbnfc2  2962  difdif  3097  ddifnel  3103  ddifstab  3104  ssddif  3198  difin  3201  uneqin  3215  indifdir  3220  undif3ss  3225  difrab  3238  un00  3290  undifss  3323  ssdifeq0  3325  ralidm  3341  ralf0  3344  ralm  3345  elpr2  3420  snidb  3424  difsnb  3528  preq12b  3562  preqsn  3567  axpweq  3945  sspwb  3971  unipw  3972  opm  3989  opth  3992  ssopab2b  4031  elon2  4131  unexb  4195  eusvnfb  4204  eusv2nf  4206  ralxfrALT  4217  uniexb  4223  iunpw  4229  sucelon  4247  unon  4255  sucprcreg  4292  opthreg  4299  ordsuc  4306  peano2b  4355  opelxp  4392  opthprc  4409  relop  4504  issetid  4508  elres  4664  iss  4674  issref  4727  xpmlem  4764  ssrnres  4783  dfrel2  4791  relrelss  4864  fn0  5038  funssxp  5080  f00  5101  dffo2  5130  ffoss  5178  f1o00  5181  fo00  5182  fv3  5218  dff2  5332  dffo4  5336  dffo5  5337  fmpt  5340  ffnfv  5344  fsn  5356  fsn2  5358  isores1  5474  ssoprab2b  5582  eqfnov2  5628  cnvoprab  5875  reldmtpos  5891  en0  6298  en1  6302  elni2  6504  ltbtwnnqq  6605  enq0ref  6623  elnp1st2nd  6666  elrealeu  6998  elreal2  6999  le2tri3i  7219  elnn0nn  8330  elnnnn0b  8332  elnnnn0c  8333  elnnz  8361  elnn0z  8364  elnnz1  8374  elz2  8419  eluz2b2  8690  elnn1uz2  8694  elioo4g  8957  eluzfz2b  9052  fzm  9057  elfz1end  9074  fzass4  9080  elfz1b  9107  nn0fz0  9133  fzolb  9162  fzom  9173  elfzo0  9191  fzo1fzo0n0  9192  elfzo0z  9193  elfzo1  9199  rexanuz  9874  rexuz3  9876  sqrt0rlem  9889  fz01or  10278  infssuzex  10345  isprm6  10526  oddpwdclemdc  10551  bdeq  10614  bdop  10666  bdunexb  10711  bj-2inf  10733  bj-nn0suc  10759