Theorem impbii 126

Description: Infer an equivalence from an implication and its converse. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
impbii.1	|- ( ph -> ps )
impbii.2	|- ( ps -> ph )

Assertion

Ref	Expression
impbii	|- ( ph <-> ps )

Proof of Theorem impbii

Step	Hyp	Ref	Expression
1		impbii.1	. 2 |- ( ph -> ps )
2		impbii.2	. 2 |- ( ps -> ph )
3		bi3 119	. 2 |- ( ( ph -> ps ) -> ( ( ps -> ph ) -> ( ph <-> ps ) ) )
4	1, 2, 3	mp2 16	1 |- ( ph <-> ps )

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  605  notnotnot  637  con2b  673  imnan  694  2false  706  pm5.21nii  709  pm4.8  712  oibabs  719  orcom  733  ioran  757  oridm  762  orbi2i  767  or12  771  pm4.44  784  ordi  821  andi  823  pm4.72  832  stdcndc  850  stdcndcOLD  851  stdcn  852  dcnn  853  pm4.82  956  rnlem  982  3jaob  1336  xoranor  1419  falantru  1445  3impexp  1480  3impexpbicom  1481  alcom  1524  19.26  1527  19.3h  1599  19.3  1600  19.21h  1603  19.43  1674  19.9h  1689  excom  1710  19.41h  1731  19.41  1732  equcom  1752  equsalh  1772  equsex  1774  cbvalv1  1797  cbvexv1  1798  cbvalh  1799  cbvexh  1801  sbbii  1811  sbh  1822  equs45f  1848  sb6f  1849  sbcof2  1856  sbequ8  1893  sbidm  1897  sb5rf  1898  sb6rf  1899  equvin  1909  sbimv  1940  cbvalvw  1966  cbvexvw  1967  sbalyz  2050  eu2  2122  eu3h  2123  eu5  2125  mo3h  2131  euan  2134  axext4  2213  cleqh  2329  r19.26  2657  ralcom3  2699  ceqsex  2838  gencbvex  2847  gencbvex2  2848  gencbval  2849  eqvinc  2926  pm13.183  2941  rr19.3v  2942  rr19.28v  2943  reu6  2992  reu3  2993  sbnfc2  3185  difdif  3329  ddifnel  3335  ddifstab  3336  ssddif  3438  difin  3441  uneqin  3455  indifdir  3460  undif3ss  3465  difrab  3478  un00  3538  undifss  3572  ssdifeq0  3574  ralidm  3592  ralf0  3594  ralm  3595  elpr2  3688  snidb  3696  difsnb  3811  preq12b  3848  preqsn  3853  axpweq  4255  exmidn0m  4285  exmidsssn  4286  exmid0el  4288  exmidel  4289  exmidundif  4290  exmidundifim  4291  sspwb  4302  unipw  4303  opm  4320  opth  4323  ssopab2b  4365  elon2  4467  unexb  4533  eusvnfb  4545  eusv2nf  4547  ralxfrALT  4558  uniexb  4564  iunpw  4571  onsucb  4595  unon  4603  sucprcreg  4641  opthreg  4648  ordsuc  4655  dcextest  4673  peano2b  4707  opelxp  4749  opthprc  4770  relop  4872  issetid  4876  xpid11  4947  elres  5041  iss  5051  issref  5111  xpmlem  5149  sqxpeq0  5152  ssrnres  5171  dfrel2  5179  relrelss  5255  fn0  5443  funssxp  5493  f00  5517  f0bi  5518  dffo2  5552  ffoss  5604  f1o00  5608  fo00  5609  fv3  5650  dff2  5779  dffo4  5783  dffo5  5784  fmpt  5785  ffnfv  5793  fsn  5807  fsn2  5809  funop  5818  isores1  5938  ssoprab2b  6061  eqfnov2  6112  cnvoprab  6380  reldmtpos  6399  mapsn  6837  mapsncnv  6842  mptelixpg  6881  elixpsn  6882  ixpsnf1o  6883  en0  6947  en1  6951  dom0  6999  exmidpw  7070  exmidpweq  7071  pw1fin  7072  exmidpw2en  7074  undifdcss  7085  residfi  7107  fidcenum  7123  djuexb  7211  ctssdc  7280  exmidomni  7309  nninfinfwlpo  7347  nninfwlpo  7348  exmidfodomr  7382  iftrueb01  7408  exmidontri  7424  exmidontri2or  7428  onntri3or  7430  onntri2or  7431  dftap2  7437  exmidmotap  7447  elni2  7501  ltbtwnnqq  7602  enq0ref  7620  elnp1st2nd  7663  elrealeu  8016  elreal2  8017  le2tri3i  8255  elnn0nn  9411  elnnnn0b  9413  elnnnn0c  9414  elnnz  9456  elnn0z  9459  elnnz1  9469  elz2  9518  eluz2b2  9798  elnn1uz2  9802  elpqb  9845  elioo4g  10130  eluzfz2b  10229  fzm  10234  elfz1end  10251  fzass4  10258  elfz1b  10286  fz01or  10307  nn0fz0  10315  fzolb  10350  fzom  10361  elfzo0  10382  fzo1fzo0n0  10383  elfzo0z  10384  elfzo1  10391  infssuzex  10453  hash2en  11065  wrdexb  11083  0wrd0  11097  rexanuz  11499  rexuz3  11501  sqrt0rlem  11514  fisum0diag  11952  fprod0diagfz  12139  isprm6  12669  oddpwdclemdc  12695  nnoddn2prmb  12785  4sqlem4  12915  4sqexercise1  12921  ennnfone  12996  ctinfom  12999  ctinf  13001  fnpr2ob  13373  dfgrp2  13560  dfgrp3m  13632  dfgrp3me  13633  isnsg3  13744  invghm  13866  dvdsrzring  14567  zrhval  14581  tgclb  14739  xmetunirn  15032  dich0  15326  elply2  15409  2sqlem2  15794  umgrislfupgrenlem  15928  umgrislfupgrdom  15929  uspgrupgrushgr  15980  usgrumgruspgr  15983  usgruspgrben  15984  usgrislfuspgrdom  15988  bj-nnsn  16097  bdeq  16186  bdop  16238  bdunexb  16283  bj-2inf  16301  bj-nn0suc  16327  nnnninfen  16387  exmidsbth  16392  trirec0  16412  redc0  16425  reap0  16426  cndcap  16427  neap0mkv  16437