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  449  jcab  593  notnotnot  624  con2b  659  imnan  680  2false  691  pm5.21nii  694  pm4.8  697  oibabs  704  orcom  718  ioran  742  oridm  747  orbi2i  752  or12  756  pm4.44  769  ordi  806  andi  808  pm4.72  817  stdcndc  835  stdcndcOLD  836  stdcn  837  dcnn  838  pm4.82  940  rnlem  966  3jaob  1292  xoranor  1367  falantru  1393  3impexp  1425  3impexpbicom  1426  alcom  1466  19.26  1469  19.3h  1541  19.3  1542  19.21h  1545  19.43  1616  19.9h  1631  excom  1652  19.41h  1673  19.41  1674  equcom  1694  equsalh  1714  equsex  1716  cbvalv1  1739  cbvexv1  1740  cbvalh  1741  cbvexh  1743  sbbii  1753  sbh  1764  equs45f  1790  sb6f  1791  sbcof2  1798  sbequ8  1835  sbidm  1839  sb5rf  1840  sb6rf  1841  equvin  1851  sbimv  1881  cbvalvw  1907  cbvexvw  1908  sbalyz  1987  eu2  2058  eu3h  2059  eu5  2061  mo3h  2067  euan  2070  axext4  2149  cleqh  2265  r19.26  2591  ralcom3  2632  ceqsex  2763  gencbvex  2771  gencbvex2  2772  gencbval  2773  eqvinc  2848  pm13.183  2863  rr19.3v  2864  rr19.28v  2865  reu6  2914  reu3  2915  sbnfc2  3104  difdif  3246  ddifnel  3252  ddifstab  3253  ssddif  3355  difin  3358  uneqin  3372  indifdir  3377  undif3ss  3382  difrab  3395  un00  3454  undifss  3488  ssdifeq0  3490  ralidm  3508  ralf0  3511  ralm  3512  elpr2  3597  snidb  3605  difsnb  3715  preq12b  3749  preqsn  3754  axpweq  4149  exmidn0m  4179  exmidsssn  4180  exmid0el  4182  exmidel  4183  exmidundif  4184  exmidundifim  4185  sspwb  4193  unipw  4194  opm  4211  opth  4214  ssopab2b  4253  elon2  4353  unexb  4419  eusvnfb  4431  eusv2nf  4433  ralxfrALT  4444  uniexb  4450  iunpw  4457  sucelon  4479  unon  4487  sucprcreg  4525  opthreg  4532  ordsuc  4539  dcextest  4557  peano2b  4591  opelxp  4633  opthprc  4654  relop  4753  issetid  4757  xpid11  4826  elres  4919  iss  4929  issref  4985  xpmlem  5023  sqxpeq0  5026  ssrnres  5045  dfrel2  5053  relrelss  5129  fn0  5306  funssxp  5356  f00  5378  f0bi  5379  dffo2  5413  ffoss  5463  f1o00  5466  fo00  5467  fv3  5508  dff2  5628  dffo4  5632  dffo5  5633  fmpt  5634  ffnfv  5642  fsn  5656  fsn2  5658  isores1  5781  ssoprab2b  5895  eqfnov2  5945  cnvoprab  6198  reldmtpos  6217  mapsn  6652  mapsncnv  6657  mptelixpg  6696  elixpsn  6697  ixpsnf1o  6698  en0  6757  en1  6761  dom0  6800  exmidpw  6870  exmidpweq  6871  pw1fin  6872  undifdcss  6884  fidcenum  6917  djuexb  7005  ctssdc  7074  exmidomni  7102  exmidfodomr  7156  exmidontri  7191  exmidontri2or  7195  onntri3or  7197  onntri2or  7198  elni2  7251  ltbtwnnqq  7352  enq0ref  7370  elnp1st2nd  7413  elrealeu  7766  elreal2  7767  le2tri3i  8003  elnn0nn  9152  elnnnn0b  9154  elnnnn0c  9155  elnnz  9197  elnn0z  9200  elnnz1  9210  elz2  9258  eluz2b2  9537  elnn1uz2  9541  elpqb  9583  elioo4g  9866  eluzfz2b  9964  fzm  9969  elfz1end  9986  fzass4  9993  elfz1b  10021  fz01or  10042  nn0fz0  10050  fzolb  10084  fzom  10095  elfzo0  10113  fzo1fzo0n0  10114  elfzo0z  10115  elfzo1  10121  rexanuz  10926  rexuz3  10928  sqrt0rlem  10941  fisum0diag  11378  fprod0diagfz  11565  infssuzex  11878  isprm6  12075  oddpwdclemdc  12101  nnoddn2prmb  12190  4sqlem4  12318  ennnfone  12354  ctinfom  12357  ctinf  12359  tgclb  12665  xmetunirn  12958  2sqlem2  13551  bj-nnsn  13574  bdeq  13665  bdop  13717  bdunexb  13762  bj-2inf  13780  bj-nn0suc  13806  exmidsbth  13863  trirec0  13883  redc0  13896  reap0  13897