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  1799  cbvexv1  1800  cbvalh  1801  cbvexh  1803  sbbii  1813  sbh  1824  equs45f  1850  sb6f  1851  sbcof2  1858  sbequ8  1895  sbidm  1899  sb5rf  1900  sb6rf  1901  equvin  1911  sbimv  1942  cbvalvw  1968  cbvexvw  1969  sbalyz  2052  eu2  2124  eu3h  2125  eu5  2127  mo3h  2133  euan  2136  axext4  2215  cleqh  2331  r19.26  2660  ralcom3  2702  ceqsex  2842  gencbvex  2851  gencbvex2  2852  gencbval  2853  eqvinc  2930  pm13.183  2945  rr19.3v  2946  rr19.28v  2947  reu6  2996  reu3  2997  sbnfc2  3189  difdif  3334  ddifnel  3340  ddifstab  3341  ssddif  3443  difin  3446  uneqin  3460  indifdir  3465  undif3ss  3470  difrab  3483  un00  3543  undifss  3577  ssdifeq0  3579  ralidm  3597  ralf0  3599  ralm  3600  elpr2  3695  snidb  3703  rabsnifsb  3741  difsnb  3821  preq12b  3858  preqsn  3863  axpweq  4267  exmidn0m  4297  exmidsssn  4298  exmid0el  4300  exmidel  4301  exmidundif  4302  exmidundifim  4303  sspwb  4314  unipw  4315  opm  4332  opth  4335  ssopab2b  4377  elon2  4479  unexb  4545  eusvnfb  4557  eusv2nf  4559  ralxfrALT  4570  uniexb  4576  iunpw  4583  onsucb  4607  unon  4615  sucprcreg  4653  opthreg  4660  ordsuc  4667  dcextest  4685  peano2b  4719  opelxp  4761  opthprc  4783  relop  4886  issetid  4890  xpid11  4961  elres  5055  iss  5065  issref  5126  xpmlem  5164  sqxpeq0  5167  ssrnres  5186  dfrel2  5194  relrelss  5270  fn0  5459  funssxp  5512  f00  5537  f0bi  5538  dffo2  5572  ffoss  5625  f1o00  5629  fo00  5630  fv3  5671  dff2  5799  dffo4  5803  dffo5  5804  fmpt  5805  ffnfv  5813  fsn  5827  fsn2  5829  funop  5839  isores1  5965  ssoprab2b  6088  eqfnov2  6139  cnvoprab  6408  reldmtpos  6462  mapsn  6902  mapsncnv  6907  mptelixpg  6946  elixpsn  6947  ixpsnf1o  6948  en0  7012  en1  7016  modom  7037  dom0  7067  exmidpw  7143  exmidpweq  7144  pw1fin  7145  exmidpw2en  7147  undifdcss  7158  exmidssfi  7174  residfi  7182  fidcenum  7198  djuexb  7303  ctssdc  7372  exmidomni  7401  nninfinfwlpo  7439  nninfwlpo  7440  exmidfodomr  7475  iftrueb01  7501  exmidontri  7517  exmidontri2or  7521  onntri3or  7523  onntri2or  7524  dftap2  7530  exmidmotap  7540  elni2  7594  ltbtwnnqq  7695  enq0ref  7713  elnp1st2nd  7756  elrealeu  8109  elreal2  8110  le2tri3i  8347  elnn0nn  9503  elnnnn0b  9505  elnnnn0c  9506  elnnz  9550  elnn0z  9553  elnnz1  9563  elz2  9612  eluz2b2  9898  elnn1uz2  9902  elpqb  9945  elioo4g  10230  eluzfz2b  10330  fzm  10335  elfz1end  10352  fzass4  10359  elfz1b  10387  fz01or  10408  nn0fz0  10416  fzolb  10451  fzom  10462  elfzo0  10483  fzo1fzo0n0  10485  elfzo0z  10486  elfzo1  10493  infssuzex  10556  hash2en  11170  wrdexb  11191  0wrd0  11205  rexanuz  11628  rexuz3  11630  sqrt0rlem  11643  fisum0diag  12082  fprod0diagfz  12269  isprm6  12799  oddpwdclemdc  12825  nnoddn2prmb  12915  4sqlem4  13045  4sqexercise1  13051  ennnfone  13126  ctinfom  13129  ctinf  13131  fnpr2ob  13503  dfgrp2  13690  dfgrp3m  13762  dfgrp3me  13763  isnsg3  13874  invghm  13996  dvdsrzring  14699  zrhval  14713  tgclb  14876  xmetunirn  15169  dich0  15463  elply2  15546  2sqlem2  15934  umgrislfupgrenlem  16071  umgrislfupgrdom  16072  uspgrupgrushgr  16123  usgrumgruspgr  16126  usgruspgrben  16127  usgrislfuspgrdom  16131  clwwlkn1loopb  16361  bj-nnsn  16451  bdeq  16539  bdop  16591  bdunexb  16636  bj-2inf  16654  bj-nn0suc  16680  pw1dceq  16726  exmidnotnotr  16727  exmidcon  16728  exmidpeirce  16729  nnnninfen  16747  exmidsbth  16752  trirec0  16776  redc0  16790  reap0  16791  cndcap  16792  neap0mkv  16802