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  1492  19.26  1495  19.3h  1567  19.3  1568  19.21h  1571  19.43  1642  19.9h  1657  excom  1678  19.41h  1699  19.41  1700  equcom  1720  equsalh  1740  equsex  1742  cbvalv1  1765  cbvexv1  1766  cbvalh  1767  cbvexh  1769  sbbii  1779  sbh  1790  equs45f  1816  sb6f  1817  sbcof2  1824  sbequ8  1861  sbidm  1865  sb5rf  1866  sb6rf  1867  equvin  1877  sbimv  1908  cbvalvw  1934  cbvexvw  1935  sbalyz  2018  eu2  2089  eu3h  2090  eu5  2092  mo3h  2098  euan  2101  axext4  2180  cleqh  2296  r19.26  2623  ralcom3  2665  ceqsex  2801  gencbvex  2810  gencbvex2  2811  gencbval  2812  eqvinc  2887  pm13.183  2902  rr19.3v  2903  rr19.28v  2904  reu6  2953  reu3  2954  sbnfc2  3145  difdif  3288  ddifnel  3294  ddifstab  3295  ssddif  3397  difin  3400  uneqin  3414  indifdir  3419  undif3ss  3424  difrab  3437  un00  3497  undifss  3531  ssdifeq0  3533  ralidm  3551  ralf0  3553  ralm  3554  elpr2  3644  snidb  3652  difsnb  3765  preq12b  3800  preqsn  3805  axpweq  4204  exmidn0m  4234  exmidsssn  4235  exmid0el  4237  exmidel  4238  exmidundif  4239  exmidundifim  4240  sspwb  4249  unipw  4250  opm  4267  opth  4270  ssopab2b  4311  elon2  4411  unexb  4477  eusvnfb  4489  eusv2nf  4491  ralxfrALT  4502  uniexb  4508  iunpw  4515  onsucb  4539  unon  4547  sucprcreg  4585  opthreg  4592  ordsuc  4599  dcextest  4617  peano2b  4651  opelxp  4693  opthprc  4714  relop  4816  issetid  4820  xpid11  4889  elres  4982  iss  4992  issref  5052  xpmlem  5090  sqxpeq0  5093  ssrnres  5112  dfrel2  5120  relrelss  5196  fn0  5377  funssxp  5427  f00  5449  f0bi  5450  dffo2  5484  ffoss  5536  f1o00  5539  fo00  5540  fv3  5581  dff2  5706  dffo4  5710  dffo5  5711  fmpt  5712  ffnfv  5720  fsn  5734  fsn2  5736  isores1  5861  ssoprab2b  5979  eqfnov2  6030  cnvoprab  6292  reldmtpos  6311  mapsn  6749  mapsncnv  6754  mptelixpg  6793  elixpsn  6794  ixpsnf1o  6795  en0  6854  en1  6858  dom0  6899  exmidpw  6969  exmidpweq  6970  pw1fin  6971  exmidpw2en  6973  undifdcss  6984  residfi  7006  fidcenum  7022  djuexb  7110  ctssdc  7179  exmidomni  7208  nninfwlpo  7245  exmidfodomr  7271  exmidontri  7306  exmidontri2or  7310  onntri3or  7312  onntri2or  7313  dftap2  7318  exmidmotap  7328  elni2  7381  ltbtwnnqq  7482  enq0ref  7500  elnp1st2nd  7543  elrealeu  7896  elreal2  7897  le2tri3i  8135  elnn0nn  9291  elnnnn0b  9293  elnnnn0c  9294  elnnz  9336  elnn0z  9339  elnnz1  9349  elz2  9397  eluz2b2  9677  elnn1uz2  9681  elpqb  9724  elioo4g  10009  eluzfz2b  10108  fzm  10113  elfz1end  10130  fzass4  10137  elfz1b  10165  fz01or  10186  nn0fz0  10194  fzolb  10229  fzom  10240  elfzo0  10258  fzo1fzo0n0  10259  elfzo0z  10260  elfzo1  10266  infssuzex  10323  wrdexb  10947  0wrd0  10961  rexanuz  11153  rexuz3  11155  sqrt0rlem  11168  fisum0diag  11606  fprod0diagfz  11793  isprm6  12315  oddpwdclemdc  12341  nnoddn2prmb  12431  4sqlem4  12561  4sqexercise1  12567  ennnfone  12642  ctinfom  12645  ctinf  12647  fnpr2ob  12983  dfgrp2  13159  dfgrp3m  13231  dfgrp3me  13232  isnsg3  13337  invghm  13459  dvdsrzring  14159  zrhval  14173  tgclb  14301  xmetunirn  14594  dich0  14888  elply2  14971  2sqlem2  15356  bj-nnsn  15379  bdeq  15469  bdop  15521  bdunexb  15566  bj-2inf  15584  bj-nn0suc  15610  nnnninfen  15665  exmidsbth  15668  trirec0  15688  redc0  15701  reap0  15702  cndcap  15703  neap0mkv  15713