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  1458  3impexpbicom  1459  alcom  1502  19.26  1505  19.3h  1577  19.3  1578  19.21h  1581  19.43  1652  19.9h  1667  excom  1688  19.41h  1709  19.41  1710  equcom  1730  equsalh  1750  equsex  1752  cbvalv1  1775  cbvexv1  1776  cbvalh  1777  cbvexh  1779  sbbii  1789  sbh  1800  equs45f  1826  sb6f  1827  sbcof2  1834  sbequ8  1871  sbidm  1875  sb5rf  1876  sb6rf  1877  equvin  1887  sbimv  1918  cbvalvw  1944  cbvexvw  1945  sbalyz  2028  eu2  2100  eu3h  2101  eu5  2103  mo3h  2109  euan  2112  axext4  2191  cleqh  2307  r19.26  2634  ralcom3  2676  ceqsex  2815  gencbvex  2824  gencbvex2  2825  gencbval  2826  eqvinc  2903  pm13.183  2918  rr19.3v  2919  rr19.28v  2920  reu6  2969  reu3  2970  sbnfc2  3162  difdif  3306  ddifnel  3312  ddifstab  3313  ssddif  3415  difin  3418  uneqin  3432  indifdir  3437  undif3ss  3442  difrab  3455  un00  3515  undifss  3549  ssdifeq0  3551  ralidm  3569  ralf0  3571  ralm  3572  elpr2  3665  snidb  3673  difsnb  3787  preq12b  3824  preqsn  3829  axpweq  4231  exmidn0m  4261  exmidsssn  4262  exmid0el  4264  exmidel  4265  exmidundif  4266  exmidundifim  4267  sspwb  4278  unipw  4279  opm  4296  opth  4299  ssopab2b  4341  elon2  4441  unexb  4507  eusvnfb  4519  eusv2nf  4521  ralxfrALT  4532  uniexb  4538  iunpw  4545  onsucb  4569  unon  4577  sucprcreg  4615  opthreg  4622  ordsuc  4629  dcextest  4647  peano2b  4681  opelxp  4723  opthprc  4744  relop  4846  issetid  4850  xpid11  4920  elres  5014  iss  5024  issref  5084  xpmlem  5122  sqxpeq0  5125  ssrnres  5144  dfrel2  5152  relrelss  5228  fn0  5415  funssxp  5465  f00  5489  f0bi  5490  dffo2  5524  ffoss  5576  f1o00  5580  fo00  5581  fv3  5622  dff2  5747  dffo4  5751  dffo5  5752  fmpt  5753  ffnfv  5761  fsn  5775  fsn2  5777  funop  5786  isores1  5906  ssoprab2b  6025  eqfnov2  6076  cnvoprab  6343  reldmtpos  6362  mapsn  6800  mapsncnv  6805  mptelixpg  6844  elixpsn  6845  ixpsnf1o  6846  en0  6910  en1  6914  dom0  6960  exmidpw  7031  exmidpweq  7032  pw1fin  7033  exmidpw2en  7035  undifdcss  7046  residfi  7068  fidcenum  7084  djuexb  7172  ctssdc  7241  exmidomni  7270  nninfinfwlpo  7308  nninfwlpo  7309  exmidfodomr  7343  iftrueb01  7369  exmidontri  7385  exmidontri2or  7389  onntri3or  7391  onntri2or  7392  dftap2  7398  exmidmotap  7408  elni2  7462  ltbtwnnqq  7563  enq0ref  7581  elnp1st2nd  7624  elrealeu  7977  elreal2  7978  le2tri3i  8216  elnn0nn  9372  elnnnn0b  9374  elnnnn0c  9375  elnnz  9417  elnn0z  9420  elnnz1  9430  elz2  9479  eluz2b2  9759  elnn1uz2  9763  elpqb  9806  elioo4g  10091  eluzfz2b  10190  fzm  10195  elfz1end  10212  fzass4  10219  elfz1b  10247  fz01or  10268  nn0fz0  10276  fzolb  10311  fzom  10322  elfzo0  10343  fzo1fzo0n0  10344  elfzo0z  10345  elfzo1  10351  infssuzex  10413  hash2en  11025  wrdexb  11043  0wrd0  11057  rexanuz  11414  rexuz3  11416  sqrt0rlem  11429  fisum0diag  11867  fprod0diagfz  12054  isprm6  12584  oddpwdclemdc  12610  nnoddn2prmb  12700  4sqlem4  12830  4sqexercise1  12836  ennnfone  12911  ctinfom  12914  ctinf  12916  fnpr2ob  13287  dfgrp2  13474  dfgrp3m  13546  dfgrp3me  13547  isnsg3  13658  invghm  13780  dvdsrzring  14480  zrhval  14494  tgclb  14652  xmetunirn  14945  dich0  15239  elply2  15322  2sqlem2  15707  umgrislfupgrenlem  15836  umgrislfupgrdom  15837  bj-nnsn  15869  bdeq  15958  bdop  16010  bdunexb  16055  bj-2inf  16073  bj-nn0suc  16099  nnnninfen  16160  exmidsbth  16165  trirec0  16185  redc0  16198  reap0  16199  cndcap  16200  neap0mkv  16210