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  3460  undifss  3494  ssdifeq0  3496  ralidm  3514  ralf0  3517  ralm  3518  elpr2  3603  snidb  3611  difsnb  3721  preq12b  3755  preqsn  3760  axpweq  4155  exmidn0m  4185  exmidsssn  4186  exmid0el  4188  exmidel  4189  exmidundif  4190  exmidundifim  4191  sspwb  4199  unipw  4200  opm  4217  opth  4220  ssopab2b  4259  elon2  4359  unexb  4425  eusvnfb  4437  eusv2nf  4439  ralxfrALT  4450  uniexb  4456  iunpw  4463  sucelon  4485  unon  4493  sucprcreg  4531  opthreg  4538  ordsuc  4545  dcextest  4563  peano2b  4597  opelxp  4639  opthprc  4660  relop  4759  issetid  4763  xpid11  4832  elres  4925  iss  4935  issref  4991  xpmlem  5029  sqxpeq0  5032  ssrnres  5051  dfrel2  5059  relrelss  5135  fn0  5315  funssxp  5365  f00  5387  f0bi  5388  dffo2  5422  ffoss  5472  f1o00  5475  fo00  5476  fv3  5517  dff2  5638  dffo4  5642  dffo5  5643  fmpt  5644  ffnfv  5652  fsn  5666  fsn2  5668  isores1  5791  ssoprab2b  5908  eqfnov2  5958  cnvoprab  6211  reldmtpos  6230  mapsn  6665  mapsncnv  6670  mptelixpg  6709  elixpsn  6710  ixpsnf1o  6711  en0  6770  en1  6774  dom0  6813  exmidpw  6883  exmidpweq  6884  pw1fin  6885  undifdcss  6897  fidcenum  6930  djuexb  7018  ctssdc  7087  exmidomni  7115  exmidfodomr  7170  exmidontri  7205  exmidontri2or  7209  onntri3or  7211  onntri2or  7212  elni2  7265  ltbtwnnqq  7366  enq0ref  7384  elnp1st2nd  7427  elrealeu  7780  elreal2  7781  le2tri3i  8017  elnn0nn  9166  elnnnn0b  9168  elnnnn0c  9169  elnnz  9211  elnn0z  9214  elnnz1  9224  elz2  9272  eluz2b2  9551  elnn1uz2  9555  elpqb  9597  elioo4g  9880  eluzfz2b  9978  fzm  9983  elfz1end  10000  fzass4  10007  elfz1b  10035  fz01or  10056  nn0fz0  10064  fzolb  10098  fzom  10109  elfzo0  10127  fzo1fzo0n0  10128  elfzo0z  10129  elfzo1  10135  rexanuz  10941  rexuz3  10943  sqrt0rlem  10956  fisum0diag  11393  fprod0diagfz  11580  infssuzex  11893  isprm6  12090  oddpwdclemdc  12116  nnoddn2prmb  12205  4sqlem4  12333  ennnfone  12369  ctinfom  12372  ctinf  12374  dfgrp2  12721  tgclb  12820  xmetunirn  13113  2sqlem2  13706  bj-nnsn  13729  bdeq  13820  bdop  13872  bdunexb  13917  bj-2inf  13935  bj-nn0suc  13961  exmidsbth  14018  trirec0  14038  redc0  14051  reap0  14052