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  1314  xoranor  1396  falantru  1422  3impexp  1456  3impexpbicom  1457  alcom  1500  19.26  1503  19.3h  1575  19.3  1576  19.21h  1579  19.43  1650  19.9h  1665  excom  1686  19.41h  1707  19.41  1708  equcom  1728  equsalh  1748  equsex  1750  cbvalv1  1773  cbvexv1  1774  cbvalh  1775  cbvexh  1777  sbbii  1787  sbh  1798  equs45f  1824  sb6f  1825  sbcof2  1832  sbequ8  1869  sbidm  1873  sb5rf  1874  sb6rf  1875  equvin  1885  sbimv  1916  cbvalvw  1942  cbvexvw  1943  sbalyz  2026  eu2  2097  eu3h  2098  eu5  2100  mo3h  2106  euan  2109  axext4  2188  cleqh  2304  r19.26  2631  ralcom3  2673  ceqsex  2809  gencbvex  2818  gencbvex2  2819  gencbval  2820  eqvinc  2895  pm13.183  2910  rr19.3v  2911  rr19.28v  2912  reu6  2961  reu3  2962  sbnfc2  3153  difdif  3297  ddifnel  3303  ddifstab  3304  ssddif  3406  difin  3409  uneqin  3423  indifdir  3428  undif3ss  3433  difrab  3446  un00  3506  undifss  3540  ssdifeq0  3542  ralidm  3560  ralf0  3562  ralm  3563  elpr2  3654  snidb  3662  difsnb  3775  preq12b  3810  preqsn  3815  axpweq  4214  exmidn0m  4244  exmidsssn  4245  exmid0el  4247  exmidel  4248  exmidundif  4249  exmidundifim  4250  sspwb  4259  unipw  4260  opm  4277  opth  4280  ssopab2b  4322  elon2  4422  unexb  4488  eusvnfb  4500  eusv2nf  4502  ralxfrALT  4513  uniexb  4519  iunpw  4526  onsucb  4550  unon  4558  sucprcreg  4596  opthreg  4603  ordsuc  4610  dcextest  4628  peano2b  4662  opelxp  4704  opthprc  4725  relop  4827  issetid  4831  xpid11  4900  elres  4994  iss  5004  issref  5064  xpmlem  5102  sqxpeq0  5105  ssrnres  5124  dfrel2  5132  relrelss  5208  fn0  5394  funssxp  5444  f00  5466  f0bi  5467  dffo2  5501  ffoss  5553  f1o00  5556  fo00  5557  fv3  5598  dff2  5723  dffo4  5727  dffo5  5728  fmpt  5729  ffnfv  5737  fsn  5751  fsn2  5753  funop  5762  isores1  5882  ssoprab2b  6001  eqfnov2  6052  cnvoprab  6319  reldmtpos  6338  mapsn  6776  mapsncnv  6781  mptelixpg  6820  elixpsn  6821  ixpsnf1o  6822  en0  6886  en1  6890  dom0  6934  exmidpw  7004  exmidpweq  7005  pw1fin  7006  exmidpw2en  7008  undifdcss  7019  residfi  7041  fidcenum  7057  djuexb  7145  ctssdc  7214  exmidomni  7243  nninfinfwlpo  7281  nninfwlpo  7282  exmidfodomr  7311  exmidontri  7350  exmidontri2or  7354  onntri3or  7356  onntri2or  7357  dftap2  7362  exmidmotap  7372  elni2  7426  ltbtwnnqq  7527  enq0ref  7545  elnp1st2nd  7588  elrealeu  7941  elreal2  7942  le2tri3i  8180  elnn0nn  9336  elnnnn0b  9338  elnnnn0c  9339  elnnz  9381  elnn0z  9384  elnnz1  9394  elz2  9443  eluz2b2  9723  elnn1uz2  9727  elpqb  9770  elioo4g  10055  eluzfz2b  10154  fzm  10159  elfz1end  10176  fzass4  10183  elfz1b  10211  fz01or  10232  nn0fz0  10240  fzolb  10275  fzom  10286  elfzo0  10304  fzo1fzo0n0  10305  elfzo0z  10306  elfzo1  10312  infssuzex  10374  hash2en  10986  wrdexb  11004  0wrd0  11018  rexanuz  11241  rexuz3  11243  sqrt0rlem  11256  fisum0diag  11694  fprod0diagfz  11881  isprm6  12411  oddpwdclemdc  12437  nnoddn2prmb  12527  4sqlem4  12657  4sqexercise1  12663  ennnfone  12738  ctinfom  12741  ctinf  12743  fnpr2ob  13114  dfgrp2  13301  dfgrp3m  13373  dfgrp3me  13374  isnsg3  13485  invghm  13607  dvdsrzring  14307  zrhval  14321  tgclb  14479  xmetunirn  14772  dich0  15066  elply2  15149  2sqlem2  15534  bj-nnsn  15602  bdeq  15692  bdop  15744  bdunexb  15789  bj-2inf  15807  bj-nn0suc  15833  nnnninfen  15891  exmidsbth  15896  trirec0  15916  redc0  15929  reap0  15930  cndcap  15931  neap0mkv  15941