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  634  con2b  669  imnan  690  2false  701  pm5.21nii  704  pm4.8  707  oibabs  714  orcom  728  ioran  752  oridm  757  orbi2i  762  or12  766  pm4.44  779  ordi  816  andi  818  pm4.72  827  stdcndc  845  stdcndcOLD  846  stdcn  847  dcnn  848  pm4.82  950  rnlem  976  3jaob  1302  xoranor  1377  falantru  1403  3impexp  1437  3impexpbicom  1438  alcom  1478  19.26  1481  19.3h  1553  19.3  1554  19.21h  1557  19.43  1628  19.9h  1643  excom  1664  19.41h  1685  19.41  1686  equcom  1706  equsalh  1726  equsex  1728  cbvalv1  1751  cbvexv1  1752  cbvalh  1753  cbvexh  1755  sbbii  1765  sbh  1776  equs45f  1802  sb6f  1803  sbcof2  1810  sbequ8  1847  sbidm  1851  sb5rf  1852  sb6rf  1853  equvin  1863  sbimv  1893  cbvalvw  1919  cbvexvw  1920  sbalyz  1999  eu2  2070  eu3h  2071  eu5  2073  mo3h  2079  euan  2082  axext4  2161  cleqh  2277  r19.26  2603  ralcom3  2645  ceqsex  2777  gencbvex  2785  gencbvex2  2786  gencbval  2787  eqvinc  2862  pm13.183  2877  rr19.3v  2878  rr19.28v  2879  reu6  2928  reu3  2929  sbnfc2  3119  difdif  3262  ddifnel  3268  ddifstab  3269  ssddif  3371  difin  3374  uneqin  3388  indifdir  3393  undif3ss  3398  difrab  3411  un00  3471  undifss  3505  ssdifeq0  3507  ralidm  3525  ralf0  3528  ralm  3529  elpr2  3616  snidb  3624  difsnb  3737  preq12b  3772  preqsn  3777  axpweq  4173  exmidn0m  4203  exmidsssn  4204  exmid0el  4206  exmidel  4207  exmidundif  4208  exmidundifim  4209  sspwb  4218  unipw  4219  opm  4236  opth  4239  ssopab2b  4278  elon2  4378  unexb  4444  eusvnfb  4456  eusv2nf  4458  ralxfrALT  4469  uniexb  4475  iunpw  4482  onsucb  4504  unon  4512  sucprcreg  4550  opthreg  4557  ordsuc  4564  dcextest  4582  peano2b  4616  opelxp  4658  opthprc  4679  relop  4779  issetid  4783  xpid11  4852  elres  4945  iss  4955  issref  5013  xpmlem  5051  sqxpeq0  5054  ssrnres  5073  dfrel2  5081  relrelss  5157  fn0  5337  funssxp  5387  f00  5409  f0bi  5410  dffo2  5444  ffoss  5495  f1o00  5498  fo00  5499  fv3  5540  dff2  5663  dffo4  5667  dffo5  5668  fmpt  5669  ffnfv  5677  fsn  5691  fsn2  5693  isores1  5818  ssoprab2b  5935  eqfnov2  5985  cnvoprab  6238  reldmtpos  6257  mapsn  6693  mapsncnv  6698  mptelixpg  6737  elixpsn  6738  ixpsnf1o  6739  en0  6798  en1  6802  dom0  6841  exmidpw  6911  exmidpweq  6912  pw1fin  6913  undifdcss  6925  fidcenum  6958  djuexb  7046  ctssdc  7115  exmidomni  7143  nninfwlpo  7180  exmidfodomr  7206  exmidontri  7241  exmidontri2or  7245  onntri3or  7247  onntri2or  7248  dftap2  7253  exmidmotap  7263  elni2  7316  ltbtwnnqq  7417  enq0ref  7435  elnp1st2nd  7478  elrealeu  7831  elreal2  7832  le2tri3i  8069  elnn0nn  9221  elnnnn0b  9223  elnnnn0c  9224  elnnz  9266  elnn0z  9269  elnnz1  9279  elz2  9327  eluz2b2  9606  elnn1uz2  9610  elpqb  9652  elioo4g  9937  eluzfz2b  10036  fzm  10041  elfz1end  10058  fzass4  10065  elfz1b  10093  fz01or  10114  nn0fz0  10122  fzolb  10156  fzom  10167  elfzo0  10185  fzo1fzo0n0  10186  elfzo0z  10187  elfzo1  10193  rexanuz  11000  rexuz3  11002  sqrt0rlem  11015  fisum0diag  11452  fprod0diagfz  11639  infssuzex  11953  isprm6  12150  oddpwdclemdc  12176  nnoddn2prmb  12265  4sqlem4  12393  ennnfone  12429  ctinfom  12432  ctinf  12434  fnpr2ob  12765  dfgrp2  12908  dfgrp3m  12975  dfgrp3me  12976  isnsg3  13073  dvdsrzring  13633  tgclb  13705  xmetunirn  13998  2sqlem2  14602  bj-nnsn  14625  bdeq  14715  bdop  14767  bdunexb  14812  bj-2inf  14830  bj-nn0suc  14856  exmidsbth  14913  trirec0  14933  redc0  14946  reap0  14947  cndcap  14948  neap0mkv  14958