Theorem impbii 125

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 118	. 2 |- ( ( ph -> ps ) -> ( ( ps -> ph ) -> ( ph <-> ps ) ) )
4	1, 2, 3	mp2 16	1 |- ( ph <-> ps )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bicom  139  biid  170  2th  173  pm5.74  178  bitri  183  bibi2i  226  bi2.04  247  pm5.4  248  imdi  249  impexp  261  ancom  264  pm4.45im  332  dfbi2  385  anass  398  pm5.32  448  jcab  592  notnotnot  623  con2b  658  imnan  679  2false  690  pm5.21nii  693  pm4.8  696  oibabs  703  orcom  717  ioran  741  oridm  746  orbi2i  751  or12  755  pm4.44  768  ordi  805  andi  807  pm4.72  812  stdcndc  830  stdcndcOLD  831  stdcn  832  dcnn  833  pm4.82  934  rnlem  960  3jaob  1280  xoranor  1355  falantru  1381  3impexp  1413  3impexpbicom  1414  alcom  1454  19.26  1457  19.3h  1532  19.3  1533  19.21h  1536  19.43  1607  19.9h  1622  excom  1642  19.41h  1663  19.41  1664  equcom  1682  equsalh  1704  equsex  1706  cbvalh  1726  cbvexh  1728  sbbii  1738  sbh  1749  equs45f  1774  sb6f  1775  sbcof2  1782  sbequ8  1819  sbidm  1823  sb5rf  1824  sb6rf  1825  equvin  1835  sbimv  1865  sbalyz  1974  eu2  2043  eu3h  2044  eu5  2046  mo3h  2052  euan  2055  axext4  2123  cleqh  2239  r19.26  2558  ralcom3  2598  ceqsex  2724  gencbvex  2732  gencbvex2  2733  gencbval  2734  eqvinc  2808  pm13.183  2822  rr19.3v  2823  rr19.28v  2824  reu6  2873  reu3  2874  sbnfc2  3060  difdif  3201  ddifnel  3207  ddifstab  3208  ssddif  3310  difin  3313  uneqin  3327  indifdir  3332  undif3ss  3337  difrab  3350  un00  3409  undifss  3443  ssdifeq0  3445  ralidm  3463  ralf0  3466  ralm  3467  elpr2  3549  snidb  3555  difsnb  3663  preq12b  3697  preqsn  3702  axpweq  4095  exmidn0m  4124  exmidsssn  4125  exmid0el  4127  exmidel  4128  exmidundif  4129  exmidundifim  4130  sspwb  4138  unipw  4139  opm  4156  opth  4159  ssopab2b  4198  elon2  4298  unexb  4363  eusvnfb  4375  eusv2nf  4377  ralxfrALT  4388  uniexb  4394  iunpw  4401  sucelon  4419  unon  4427  sucprcreg  4464  opthreg  4471  ordsuc  4478  dcextest  4495  peano2b  4528  opelxp  4569  opthprc  4590  relop  4689  issetid  4693  xpid11  4762  elres  4855  iss  4865  issref  4921  xpmlem  4959  sqxpeq0  4962  ssrnres  4981  dfrel2  4989  relrelss  5065  fn0  5242  funssxp  5292  f00  5314  f0bi  5315  dffo2  5349  ffoss  5399  f1o00  5402  fo00  5403  fv3  5444  dff2  5564  dffo4  5568  dffo5  5569  fmpt  5570  ffnfv  5578  fsn  5592  fsn2  5594  isores1  5715  ssoprab2b  5828  eqfnov2  5878  cnvoprab  6131  reldmtpos  6150  mapsn  6584  mapsncnv  6589  mptelixpg  6628  elixpsn  6629  ixpsnf1o  6630  en0  6689  en1  6693  dom0  6732  exmidpw  6802  undifdcss  6811  fidcenum  6844  djuexb  6929  ctssdc  6998  exmidomni  7014  exmidfodomr  7060  elni2  7122  ltbtwnnqq  7223  enq0ref  7241  elnp1st2nd  7284  elrealeu  7637  elreal2  7638  le2tri3i  7872  elnn0nn  9019  elnnnn0b  9021  elnnnn0c  9022  elnnz  9064  elnn0z  9067  elnnz1  9077  elz2  9122  eluz2b2  9397  elnn1uz2  9401  elioo4g  9717  eluzfz2b  9813  fzm  9818  elfz1end  9835  fzass4  9842  elfz1b  9870  fz01or  9891  nn0fz0  9899  fzolb  9930  fzom  9941  elfzo0  9959  fzo1fzo0n0  9960  elfzo0z  9961  elfzo1  9967  rexanuz  10760  rexuz3  10762  sqrt0rlem  10775  fisum0diag  11210  infssuzex  11642  isprm6  11825  oddpwdclemdc  11851  ennnfone  11938  ctinfom  11941  ctinf  11943  tgclb  12234  xmetunirn  12527  bj-nnsn  12945  bdeq  13021  bdop  13073  bdunexb  13118  bj-2inf  13136  bj-nn0suc  13162  exmidsbth  13219