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  635  con2b  670  imnan  691  2false  702  pm5.21nii  705  pm4.8  708  oibabs  715  orcom  729  ioran  753  oridm  758  orbi2i  763  or12  767  pm4.44  780  ordi  817  andi  819  pm4.72  828  stdcndc  846  stdcndcOLD  847  stdcn  848  dcnn  849  pm4.82  952  rnlem  978  3jaob  1313  xoranor  1388  falantru  1414  3impexp  1448  3impexpbicom  1449  alcom  1489  19.26  1492  19.3h  1564  19.3  1565  19.21h  1568  19.43  1639  19.9h  1654  excom  1675  19.41h  1696  19.41  1697  equcom  1717  equsalh  1737  equsex  1739  cbvalv1  1762  cbvexv1  1763  cbvalh  1764  cbvexh  1766  sbbii  1776  sbh  1787  equs45f  1813  sb6f  1814  sbcof2  1821  sbequ8  1858  sbidm  1862  sb5rf  1863  sb6rf  1864  equvin  1874  sbimv  1905  cbvalvw  1931  cbvexvw  1932  sbalyz  2011  eu2  2082  eu3h  2083  eu5  2085  mo3h  2091  euan  2094  axext4  2173  cleqh  2289  r19.26  2616  ralcom3  2658  ceqsex  2790  gencbvex  2798  gencbvex2  2799  gencbval  2800  eqvinc  2875  pm13.183  2890  rr19.3v  2891  rr19.28v  2892  reu6  2941  reu3  2942  sbnfc2  3132  difdif  3275  ddifnel  3281  ddifstab  3282  ssddif  3384  difin  3387  uneqin  3401  indifdir  3406  undif3ss  3411  difrab  3424  un00  3484  undifss  3518  ssdifeq0  3520  ralidm  3538  ralf0  3541  ralm  3542  elpr2  3629  snidb  3637  difsnb  3750  preq12b  3785  preqsn  3790  axpweq  4189  exmidn0m  4219  exmidsssn  4220  exmid0el  4222  exmidel  4223  exmidundif  4224  exmidundifim  4225  sspwb  4234  unipw  4235  opm  4252  opth  4255  ssopab2b  4294  elon2  4394  unexb  4460  eusvnfb  4472  eusv2nf  4474  ralxfrALT  4485  uniexb  4491  iunpw  4498  onsucb  4520  unon  4528  sucprcreg  4566  opthreg  4573  ordsuc  4580  dcextest  4598  peano2b  4632  opelxp  4674  opthprc  4695  relop  4795  issetid  4799  xpid11  4868  elres  4961  iss  4971  issref  5029  xpmlem  5067  sqxpeq0  5070  ssrnres  5089  dfrel2  5097  relrelss  5173  fn0  5354  funssxp  5404  f00  5426  f0bi  5427  dffo2  5461  ffoss  5512  f1o00  5515  fo00  5516  fv3  5557  dff2  5681  dffo4  5685  dffo5  5686  fmpt  5687  ffnfv  5695  fsn  5709  fsn2  5711  isores1  5836  ssoprab2b  5953  eqfnov2  6004  cnvoprab  6259  reldmtpos  6278  mapsn  6716  mapsncnv  6721  mptelixpg  6760  elixpsn  6761  ixpsnf1o  6762  en0  6821  en1  6825  dom0  6866  exmidpw  6936  exmidpweq  6937  pw1fin  6938  exmidpw2en  6940  undifdcss  6951  fidcenum  6985  djuexb  7073  ctssdc  7142  exmidomni  7170  nninfwlpo  7207  exmidfodomr  7233  exmidontri  7268  exmidontri2or  7272  onntri3or  7274  onntri2or  7275  dftap2  7280  exmidmotap  7290  elni2  7343  ltbtwnnqq  7444  enq0ref  7462  elnp1st2nd  7505  elrealeu  7858  elreal2  7859  le2tri3i  8096  elnn0nn  9248  elnnnn0b  9250  elnnnn0c  9251  elnnz  9293  elnn0z  9296  elnnz1  9306  elz2  9354  eluz2b2  9633  elnn1uz2  9637  elpqb  9679  elioo4g  9964  eluzfz2b  10063  fzm  10068  elfz1end  10085  fzass4  10092  elfz1b  10120  fz01or  10141  nn0fz0  10149  fzolb  10183  fzom  10194  elfzo0  10212  fzo1fzo0n0  10213  elfzo0z  10214  elfzo1  10220  rexanuz  11029  rexuz3  11031  sqrt0rlem  11044  fisum0diag  11481  fprod0diagfz  11668  infssuzex  11982  isprm6  12179  oddpwdclemdc  12205  nnoddn2prmb  12294  4sqlem4  12424  4sqexercise1  12430  ennnfone  12476  ctinfom  12479  ctinf  12481  fnpr2ob  12816  dfgrp2  12971  dfgrp3m  13043  dfgrp3me  13044  isnsg3  13146  dvdsrzring  13902  tgclb  14022  xmetunirn  14315  2sqlem2  14920  bj-nnsn  14943  bdeq  15033  bdop  15085  bdunexb  15130  bj-2inf  15148  bj-nn0suc  15174  exmidsbth  15231  trirec0  15251  redc0  15264  reap0  15265  cndcap  15266  neap0mkv  15276