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  607  notnotnot  639  con2b  675  imnan  697  2false  709  pm5.21nii  712  pm4.8  715  oibabs  722  orcom  736  ioran  760  oridm  765  orbi2i  770  or12  774  pm4.44  787  ordi  824  andi  826  pm4.72  835  stdcndc  853  stdcndcOLD  854  stdcn  855  dcnn  856  pm4.82  959  rnlem  985  3jaob  1339  xoranor  1422  falantru  1448  3impexp  1483  3impexpbicom  1484  alcom  1527  19.26  1530  19.3h  1602  19.3  1603  19.21h  1606  19.43  1677  19.9h  1692  excom  1712  19.41h  1733  19.41  1734  equcom  1754  equsalh  1774  equsex  1776  cbvalv1  1800  cbvexv1  1801  cbvalh  1802  cbvexh  1804  sbbii  1814  sbh  1825  equs45f  1851  sb6f  1852  sbcof2  1859  sbequ8  1896  sbidm  1900  sb5rf  1901  sb6rf  1902  equvin  1912  sbimv  1944  cbvalvw  1971  cbvexvw  1972  sbalyz  2055  eu2  2127  eu3h  2128  eu5  2130  mo3h  2136  euan  2139  axext4  2218  cleqh  2334  r19.26  2671  ralcom3  2713  ceqsex  2854  gencbvex  2863  gencbvex2  2864  gencbval  2865  eqvinc  2942  pm13.183  2957  rr19.3v  2958  rr19.28v  2959  reu6  3008  reu3  3009  sbnfc2  3201  difdif  3346  ddifnel  3352  ddifstab  3353  ssddif  3457  difin  3460  uneqin  3474  indifdir  3479  undif3ss  3484  difrab  3497  un00  3557  undifss  3592  ssdifeq0  3594  ralidm  3612  ralf0  3614  ralm  3615  elpr2  3713  snidb  3721  rabsnifsb  3759  difsnb  3839  preq12b  3876  preqsn  3881  axpweq  4286  exmidn0m  4316  exmidsssn  4317  exmid0el  4319  exmidel  4320  exmidundif  4321  exmidundifim  4322  sspwb  4334  unipw  4335  opm  4352  opth  4355  ssopab2b  4397  elon2  4499  unexb  4565  eusvnfb  4577  eusv2nf  4579  ralxfrALT  4590  uniexb  4596  iunpw  4603  onsucb  4627  unon  4635  sucprcreg  4673  opthreg  4680  ordsuc  4687  dcextest  4705  peano2b  4739  opelxp  4781  opthprc  4803  relop  4907  issetid  4911  xpid11  4982  elres  5076  iss  5086  issref  5147  xpmlem  5185  sqxpeq0  5188  ssrnres  5207  dfrel2  5215  relrelss  5291  fn0  5480  funssxp  5534  f00  5561  f0bi  5562  dffo2  5596  ffoss  5649  f1o00  5653  fo00  5654  fv3  5695  dff2  5823  dffo4  5827  dffo5  5828  fmpt  5829  ffnfv  5837  fsn  5851  fsn2  5853  funop  5863  isores1  5989  ssoprab2b  6112  eqfnov2  6163  cnvoprab  6432  reldmtpos  6486  mapsn  6927  mapsncnv  6932  mptelixpg  6971  elixpsn  6972  ixpsnf1o  6973  en0  7037  en1  7041  modom  7063  dom0  7093  exmidpw  7170  exmidpweq  7171  pw1fin  7172  exmidpw2en  7174  undifdcss  7185  exmidssfi  7201  residfi  7209  fidcenum  7228  djuexb  7337  ctssdc  7406  exmidomni  7435  nninfinfwlpo  7473  nninfwlpo  7474  exmidfodomr  7509  iftrueb01  7535  exmidontri  7551  exmidontri2or  7555  onntri3or  7557  onntri2or  7558  dftap2  7567  exmidmotap  7577  elni2  7631  ltbtwnnqq  7732  enq0ref  7750  elnp1st2nd  7793  elrealeu  8146  elreal2  8147  le2tri3i  8384  elnn0nn  9540  elnnnn0b  9542  elnnnn0c  9543  elnnz  9589  elnn0z  9592  elnnz1  9602  elz2  9651  eluz2b2  9938  elnn1uz2  9942  elpqb  9985  elioo4g  10270  eluzfz2b  10370  fzm  10375  elfz1end  10392  fzass4  10399  elfz1b  10428  fz01or  10449  nn0fz0  10457  fzolb  10492  fzom  10503  elfzo0  10524  fzo1fzo0n0  10526  elfzo0z  10527  elfzo1  10534  infssuzex  10597  hash2en  11219  wrdexb  11240  0wrd0  11254  rexanuz  11677  rexuz3  11679  sqrt0rlem  11692  fisum0diag  12131  fprod0diagfz  12318  isprm6  12848  oddpwdclemdc  12874  nnoddn2prmb  12964  4sqlem4  13094  4sqexercise1  13100  ballotfilem2  13149  ennnfone  13193  ctinfom  13196  ctinf  13198  fnpr2ob  13570  dfgrp2  13757  dfgrp3m  13829  dfgrp3me  13830  isnsg3  13941  invghm  14063  dvdsrzring  14768  zrhval  14782  tgclb  14947  xmetunirn  15240  dich0  15534  elply2  15617  2sqlem2  16005  umgrislfupgrenlem  16142  umgrislfupgrdom  16143  uspgrupgrushgr  16194  usgrumgruspgr  16197  usgruspgrben  16198  usgrislfuspgrdom  16202  clwwlkn1loopb  16432  bj-nnsn  16522  bdeq  16610  bdop  16662  bdunexb  16707  bj-2inf  16725  bj-nn0suc  16751  pw1dceq  16795  exmidnotnotr  16796  exmidcon  16797  exmidpeirce  16798  nnnninfen  16816  exmidsbth  16821  trirec0  16845  redc0  16859  reap0  16860  cndcap  16861  neap0mkv  16872