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  2776  gencbvex  2784  gencbvex2  2785  gencbval  2786  eqvinc  2861  pm13.183  2876  rr19.3v  2877  rr19.28v  2878  reu6  2927  reu3  2928  sbnfc2  3118  difdif  3261  ddifnel  3267  ddifstab  3268  ssddif  3370  difin  3373  uneqin  3387  indifdir  3392  undif3ss  3397  difrab  3410  un00  3470  undifss  3504  ssdifeq0  3506  ralidm  3524  ralf0  3527  ralm  3528  elpr2  3615  snidb  3623  difsnb  3736  preq12b  3771  preqsn  3776  axpweq  4172  exmidn0m  4202  exmidsssn  4203  exmid0el  4205  exmidel  4206  exmidundif  4207  exmidundifim  4208  sspwb  4217  unipw  4218  opm  4235  opth  4238  ssopab2b  4277  elon2  4377  unexb  4443  eusvnfb  4455  eusv2nf  4457  ralxfrALT  4468  uniexb  4474  iunpw  4481  onsucb  4503  unon  4511  sucprcreg  4549  opthreg  4556  ordsuc  4563  dcextest  4581  peano2b  4615  opelxp  4657  opthprc  4678  relop  4778  issetid  4782  xpid11  4851  elres  4944  iss  4954  issref  5012  xpmlem  5050  sqxpeq0  5053  ssrnres  5072  dfrel2  5080  relrelss  5156  fn0  5336  funssxp  5386  f00  5408  f0bi  5409  dffo2  5443  ffoss  5494  f1o00  5497  fo00  5498  fv3  5539  dff2  5661  dffo4  5665  dffo5  5666  fmpt  5667  ffnfv  5675  fsn  5689  fsn2  5691  isores1  5815  ssoprab2b  5932  eqfnov2  5982  cnvoprab  6235  reldmtpos  6254  mapsn  6690  mapsncnv  6695  mptelixpg  6734  elixpsn  6735  ixpsnf1o  6736  en0  6795  en1  6799  dom0  6838  exmidpw  6908  exmidpweq  6909  pw1fin  6910  undifdcss  6922  fidcenum  6955  djuexb  7043  ctssdc  7112  exmidomni  7140  nninfwlpo  7177  exmidfodomr  7203  exmidontri  7238  exmidontri2or  7242  onntri3or  7244  onntri2or  7245  dftap2  7250  exmidmotap  7260  elni2  7313  ltbtwnnqq  7414  enq0ref  7432  elnp1st2nd  7475  elrealeu  7828  elreal2  7829  le2tri3i  8066  elnn0nn  9218  elnnnn0b  9220  elnnnn0c  9221  elnnz  9263  elnn0z  9266  elnnz1  9276  elz2  9324  eluz2b2  9603  elnn1uz2  9607  elpqb  9649  elioo4g  9934  eluzfz2b  10033  fzm  10038  elfz1end  10055  fzass4  10062  elfz1b  10090  fz01or  10111  nn0fz0  10119  fzolb  10153  fzom  10164  elfzo0  10182  fzo1fzo0n0  10183  elfzo0z  10184  elfzo1  10190  rexanuz  10997  rexuz3  10999  sqrt0rlem  11012  fisum0diag  11449  fprod0diagfz  11636  infssuzex  11950  isprm6  12147  oddpwdclemdc  12173  nnoddn2prmb  12262  4sqlem4  12390  ennnfone  12426  ctinfom  12429  ctinf  12431  fnpr2ob  12759  dfgrp2  12902  dfgrp3m  12969  dfgrp3me  12970  isnsg3  13067  dvdsrzring  13496  tgclb  13568  xmetunirn  13861  2sqlem2  14465  bj-nnsn  14488  bdeq  14578  bdop  14630  bdunexb  14675  bj-2inf  14693  bj-nn0suc  14719  exmidsbth  14775  trirec0  14795  redc0  14808  reap0  14809  neap0mkv  14819