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  386  anass  399  pm5.32  450  jcab  598  notnotnot  629  con2b  664  imnan  685  2false  696  pm5.21nii  699  pm4.8  702  oibabs  709  orcom  723  ioran  747  oridm  752  orbi2i  757  or12  761  pm4.44  774  ordi  811  andi  813  pm4.72  822  stdcndc  840  stdcndcOLD  841  stdcn  842  dcnn  843  pm4.82  945  rnlem  971  3jaob  1297  xoranor  1372  falantru  1398  3impexp  1430  3impexpbicom  1431  alcom  1471  19.26  1474  19.3h  1546  19.3  1547  19.21h  1550  19.43  1621  19.9h  1636  excom  1657  19.41h  1678  19.41  1679  equcom  1699  equsalh  1719  equsex  1721  cbvalv1  1744  cbvexv1  1745  cbvalh  1746  cbvexh  1748  sbbii  1758  sbh  1769  equs45f  1795  sb6f  1796  sbcof2  1803  sbequ8  1840  sbidm  1844  sb5rf  1845  sb6rf  1846  equvin  1856  sbimv  1886  cbvalvw  1912  cbvexvw  1913  sbalyz  1992  eu2  2063  eu3h  2064  eu5  2066  mo3h  2072  euan  2075  axext4  2154  cleqh  2270  r19.26  2596  ralcom3  2637  ceqsex  2768  gencbvex  2776  gencbvex2  2777  gencbval  2778  eqvinc  2853  pm13.183  2868  rr19.3v  2869  rr19.28v  2870  reu6  2919  reu3  2920  sbnfc2  3109  difdif  3252  ddifnel  3258  ddifstab  3259  ssddif  3361  difin  3364  uneqin  3378  indifdir  3383  undif3ss  3388  difrab  3401  un00  3461  undifss  3495  ssdifeq0  3497  ralidm  3515  ralf0  3518  ralm  3519  elpr2  3605  snidb  3613  difsnb  3723  preq12b  3757  preqsn  3762  axpweq  4157  exmidn0m  4187  exmidsssn  4188  exmid0el  4190  exmidel  4191  exmidundif  4192  exmidundifim  4193  sspwb  4201  unipw  4202  opm  4219  opth  4222  ssopab2b  4261  elon2  4361  unexb  4427  eusvnfb  4439  eusv2nf  4441  ralxfrALT  4452  uniexb  4458  iunpw  4465  sucelon  4487  unon  4495  sucprcreg  4533  opthreg  4540  ordsuc  4547  dcextest  4565  peano2b  4599  opelxp  4641  opthprc  4662  relop  4761  issetid  4765  xpid11  4834  elres  4927  iss  4937  issref  4993  xpmlem  5031  sqxpeq0  5034  ssrnres  5053  dfrel2  5061  relrelss  5137  fn0  5317  funssxp  5367  f00  5389  f0bi  5390  dffo2  5424  ffoss  5474  f1o00  5477  fo00  5478  fv3  5519  dff2  5640  dffo4  5644  dffo5  5645  fmpt  5646  ffnfv  5654  fsn  5668  fsn2  5670  isores1  5793  ssoprab2b  5910  eqfnov2  5960  cnvoprab  6213  reldmtpos  6232  mapsn  6668  mapsncnv  6673  mptelixpg  6712  elixpsn  6713  ixpsnf1o  6714  en0  6773  en1  6777  dom0  6816  exmidpw  6886  exmidpweq  6887  pw1fin  6888  undifdcss  6900  fidcenum  6933  djuexb  7021  ctssdc  7090  exmidomni  7118  nninfwlpo  7155  exmidfodomr  7181  exmidontri  7216  exmidontri2or  7220  onntri3or  7222  onntri2or  7223  elni2  7276  ltbtwnnqq  7377  enq0ref  7395  elnp1st2nd  7438  elrealeu  7791  elreal2  7792  le2tri3i  8028  elnn0nn  9177  elnnnn0b  9179  elnnnn0c  9180  elnnz  9222  elnn0z  9225  elnnz1  9235  elz2  9283  eluz2b2  9562  elnn1uz2  9566  elpqb  9608  elioo4g  9891  eluzfz2b  9989  fzm  9994  elfz1end  10011  fzass4  10018  elfz1b  10046  fz01or  10067  nn0fz0  10075  fzolb  10109  fzom  10120  elfzo0  10138  fzo1fzo0n0  10139  elfzo0z  10140  elfzo1  10146  rexanuz  10952  rexuz3  10954  sqrt0rlem  10967  fisum0diag  11404  fprod0diagfz  11591  infssuzex  11904  isprm6  12101  oddpwdclemdc  12127  nnoddn2prmb  12216  4sqlem4  12344  ennnfone  12380  ctinfom  12383  ctinf  12385  dfgrp2  12732  tgclb  12859  xmetunirn  13152  2sqlem2  13745  bj-nnsn  13768  bdeq  13858  bdop  13910  bdunexb  13955  bj-2inf  13973  bj-nn0suc  13999  exmidsbth  14056  trirec0  14076  redc0  14089  reap0  14090