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  603  notnotnot  635  con2b  671  imnan  692  2false  703  pm5.21nii  706  pm4.8  709  oibabs  716  orcom  730  ioran  754  oridm  759  orbi2i  764  or12  768  pm4.44  781  ordi  818  andi  820  pm4.72  829  stdcndc  847  stdcndcOLD  848  stdcn  849  dcnn  850  pm4.82  953  rnlem  979  3jaob  1315  xoranor  1397  falantru  1423  3impexp  1457  3impexpbicom  1458  alcom  1501  19.26  1504  19.3h  1576  19.3  1577  19.21h  1580  19.43  1651  19.9h  1666  excom  1687  19.41h  1708  19.41  1709  equcom  1729  equsalh  1749  equsex  1751  cbvalv1  1774  cbvexv1  1775  cbvalh  1776  cbvexh  1778  sbbii  1788  sbh  1799  equs45f  1825  sb6f  1826  sbcof2  1833  sbequ8  1870  sbidm  1874  sb5rf  1875  sb6rf  1876  equvin  1886  sbimv  1917  cbvalvw  1943  cbvexvw  1944  sbalyz  2027  eu2  2098  eu3h  2099  eu5  2101  mo3h  2107  euan  2110  axext4  2189  cleqh  2305  r19.26  2632  ralcom3  2674  ceqsex  2810  gencbvex  2819  gencbvex2  2820  gencbval  2821  eqvinc  2896  pm13.183  2911  rr19.3v  2912  rr19.28v  2913  reu6  2962  reu3  2963  sbnfc2  3154  difdif  3298  ddifnel  3304  ddifstab  3305  ssddif  3407  difin  3410  uneqin  3424  indifdir  3429  undif3ss  3434  difrab  3447  un00  3507  undifss  3541  ssdifeq0  3543  ralidm  3561  ralf0  3563  ralm  3564  elpr2  3655  snidb  3663  difsnb  3776  preq12b  3811  preqsn  3816  axpweq  4215  exmidn0m  4245  exmidsssn  4246  exmid0el  4248  exmidel  4249  exmidundif  4250  exmidundifim  4251  sspwb  4260  unipw  4261  opm  4278  opth  4281  ssopab2b  4323  elon2  4423  unexb  4489  eusvnfb  4501  eusv2nf  4503  ralxfrALT  4514  uniexb  4520  iunpw  4527  onsucb  4551  unon  4559  sucprcreg  4597  opthreg  4604  ordsuc  4611  dcextest  4629  peano2b  4663  opelxp  4705  opthprc  4726  relop  4828  issetid  4832  xpid11  4901  elres  4995  iss  5005  issref  5065  xpmlem  5103  sqxpeq0  5106  ssrnres  5125  dfrel2  5133  relrelss  5209  fn0  5395  funssxp  5445  f00  5467  f0bi  5468  dffo2  5502  ffoss  5554  f1o00  5557  fo00  5558  fv3  5599  dff2  5724  dffo4  5728  dffo5  5729  fmpt  5730  ffnfv  5738  fsn  5752  fsn2  5754  funop  5763  isores1  5883  ssoprab2b  6002  eqfnov2  6053  cnvoprab  6320  reldmtpos  6339  mapsn  6777  mapsncnv  6782  mptelixpg  6821  elixpsn  6822  ixpsnf1o  6823  en0  6887  en1  6891  dom0  6935  exmidpw  7005  exmidpweq  7006  pw1fin  7007  exmidpw2en  7009  undifdcss  7020  residfi  7042  fidcenum  7058  djuexb  7146  ctssdc  7215  exmidomni  7244  nninfinfwlpo  7282  nninfwlpo  7283  exmidfodomr  7312  exmidontri  7351  exmidontri2or  7355  onntri3or  7357  onntri2or  7358  dftap2  7363  exmidmotap  7373  elni2  7427  ltbtwnnqq  7528  enq0ref  7546  elnp1st2nd  7589  elrealeu  7942  elreal2  7943  le2tri3i  8181  elnn0nn  9337  elnnnn0b  9339  elnnnn0c  9340  elnnz  9382  elnn0z  9385  elnnz1  9395  elz2  9444  eluz2b2  9724  elnn1uz2  9728  elpqb  9771  elioo4g  10056  eluzfz2b  10155  fzm  10160  elfz1end  10177  fzass4  10184  elfz1b  10212  fz01or  10233  nn0fz0  10241  fzolb  10276  fzom  10287  elfzo0  10306  fzo1fzo0n0  10307  elfzo0z  10308  elfzo1  10314  infssuzex  10376  hash2en  10988  wrdexb  11006  0wrd0  11020  rexanuz  11299  rexuz3  11301  sqrt0rlem  11314  fisum0diag  11752  fprod0diagfz  11939  isprm6  12469  oddpwdclemdc  12495  nnoddn2prmb  12585  4sqlem4  12715  4sqexercise1  12721  ennnfone  12796  ctinfom  12799  ctinf  12801  fnpr2ob  13172  dfgrp2  13359  dfgrp3m  13431  dfgrp3me  13432  isnsg3  13543  invghm  13665  dvdsrzring  14365  zrhval  14379  tgclb  14537  xmetunirn  14830  dich0  15124  elply2  15207  2sqlem2  15592  bj-nnsn  15669  bdeq  15759  bdop  15811  bdunexb  15856  bj-2inf  15874  bj-nn0suc  15900  nnnninfen  15958  exmidsbth  15963  trirec0  15983  redc0  15996  reap0  15997  cndcap  15998  neap0mkv  16008