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  4216  exmidn0m  4246  exmidsssn  4247  exmid0el  4249  exmidel  4250  exmidundif  4251  exmidundifim  4252  sspwb  4261  unipw  4262  opm  4279  opth  4282  ssopab2b  4324  elon2  4424  unexb  4490  eusvnfb  4502  eusv2nf  4504  ralxfrALT  4515  uniexb  4521  iunpw  4528  onsucb  4552  unon  4560  sucprcreg  4598  opthreg  4605  ordsuc  4612  dcextest  4630  peano2b  4664  opelxp  4706  opthprc  4727  relop  4829  issetid  4833  xpid11  4902  elres  4996  iss  5006  issref  5066  xpmlem  5104  sqxpeq0  5107  ssrnres  5126  dfrel2  5134  relrelss  5210  fn0  5397  funssxp  5447  f00  5469  f0bi  5470  dffo2  5504  ffoss  5556  f1o00  5559  fo00  5560  fv3  5601  dff2  5726  dffo4  5730  dffo5  5731  fmpt  5732  ffnfv  5740  fsn  5754  fsn2  5756  funop  5765  isores1  5885  ssoprab2b  6004  eqfnov2  6055  cnvoprab  6322  reldmtpos  6341  mapsn  6779  mapsncnv  6784  mptelixpg  6823  elixpsn  6824  ixpsnf1o  6825  en0  6889  en1  6893  dom0  6937  exmidpw  7007  exmidpweq  7008  pw1fin  7009  exmidpw2en  7011  undifdcss  7022  residfi  7044  fidcenum  7060  djuexb  7148  ctssdc  7217  exmidomni  7246  nninfinfwlpo  7284  nninfwlpo  7285  exmidfodomr  7314  exmidontri  7353  exmidontri2or  7357  onntri3or  7359  onntri2or  7360  dftap2  7365  exmidmotap  7375  elni2  7429  ltbtwnnqq  7530  enq0ref  7548  elnp1st2nd  7591  elrealeu  7944  elreal2  7945  le2tri3i  8183  elnn0nn  9339  elnnnn0b  9341  elnnnn0c  9342  elnnz  9384  elnn0z  9387  elnnz1  9397  elz2  9446  eluz2b2  9726  elnn1uz2  9730  elpqb  9773  elioo4g  10058  eluzfz2b  10157  fzm  10162  elfz1end  10179  fzass4  10186  elfz1b  10214  fz01or  10235  nn0fz0  10243  fzolb  10278  fzom  10289  elfzo0  10308  fzo1fzo0n0  10309  elfzo0z  10310  elfzo1  10316  infssuzex  10378  hash2en  10990  wrdexb  11008  0wrd0  11022  rexanuz  11332  rexuz3  11334  sqrt0rlem  11347  fisum0diag  11785  fprod0diagfz  11972  isprm6  12502  oddpwdclemdc  12528  nnoddn2prmb  12618  4sqlem4  12748  4sqexercise1  12754  ennnfone  12829  ctinfom  12832  ctinf  12834  fnpr2ob  13205  dfgrp2  13392  dfgrp3m  13464  dfgrp3me  13465  isnsg3  13576  invghm  13698  dvdsrzring  14398  zrhval  14412  tgclb  14570  xmetunirn  14863  dich0  15157  elply2  15240  2sqlem2  15625  bj-nnsn  15706  bdeq  15796  bdop  15848  bdunexb  15893  bj-2inf  15911  bj-nn0suc  15937  nnnninfen  15995  exmidsbth  16000  trirec0  16020  redc0  16033  reap0  16034  cndcap  16035  neap0mkv  16045