Theorem impbii 125

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 118	. 2 |- ( ( ph -> ps ) -> ( ( ps -> ph ) -> ( ph <-> ps ) ) )
4	1, 2, 3	mp2 16	1 |- ( ph <-> ps )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bicom  139  biid  170  2th  173  pm5.74  178  bitri  183  bibi2i  226  bi2.04  247  pm5.4  248  imdi  249  impexp  261  ancom  264  pm4.45im  332  dfbi2  386  anass  399  pm5.32  449  jcab  593  notnotnot  624  con2b  659  imnan  680  2false  691  pm5.21nii  694  pm4.8  697  oibabs  704  orcom  718  ioran  742  oridm  747  orbi2i  752  or12  756  pm4.44  769  ordi  806  andi  808  pm4.72  813  stdcndc  831  stdcndcOLD  832  stdcn  833  dcnn  834  pm4.82  935  rnlem  961  3jaob  1281  xoranor  1356  falantru  1382  3impexp  1414  3impexpbicom  1415  alcom  1455  19.26  1458  19.3h  1533  19.3  1534  19.21h  1537  19.43  1608  19.9h  1623  excom  1643  19.41h  1664  19.41  1665  equcom  1683  equsalh  1705  equsex  1707  cbvalh  1727  cbvexh  1729  sbbii  1739  sbh  1750  equs45f  1775  sb6f  1776  sbcof2  1783  sbequ8  1820  sbidm  1824  sb5rf  1825  sb6rf  1826  equvin  1836  sbimv  1866  sbalyz  1975  eu2  2044  eu3h  2045  eu5  2047  mo3h  2053  euan  2056  axext4  2124  cleqh  2240  r19.26  2561  ralcom3  2601  ceqsex  2727  gencbvex  2735  gencbvex2  2736  gencbval  2737  eqvinc  2812  pm13.183  2826  rr19.3v  2827  rr19.28v  2828  reu6  2877  reu3  2878  sbnfc2  3065  difdif  3206  ddifnel  3212  ddifstab  3213  ssddif  3315  difin  3318  uneqin  3332  indifdir  3337  undif3ss  3342  difrab  3355  un00  3414  undifss  3448  ssdifeq0  3450  ralidm  3468  ralf0  3471  ralm  3472  elpr2  3554  snidb  3562  difsnb  3671  preq12b  3705  preqsn  3710  axpweq  4103  exmidn0m  4132  exmidsssn  4133  exmid0el  4135  exmidel  4136  exmidundif  4137  exmidundifim  4138  sspwb  4146  unipw  4147  opm  4164  opth  4167  ssopab2b  4206  elon2  4306  unexb  4371  eusvnfb  4383  eusv2nf  4385  ralxfrALT  4396  uniexb  4402  iunpw  4409  sucelon  4427  unon  4435  sucprcreg  4472  opthreg  4479  ordsuc  4486  dcextest  4503  peano2b  4536  opelxp  4577  opthprc  4598  relop  4697  issetid  4701  xpid11  4770  elres  4863  iss  4873  issref  4929  xpmlem  4967  sqxpeq0  4970  ssrnres  4989  dfrel2  4997  relrelss  5073  fn0  5250  funssxp  5300  f00  5322  f0bi  5323  dffo2  5357  ffoss  5407  f1o00  5410  fo00  5411  fv3  5452  dff2  5572  dffo4  5576  dffo5  5577  fmpt  5578  ffnfv  5586  fsn  5600  fsn2  5602  isores1  5723  ssoprab2b  5836  eqfnov2  5886  cnvoprab  6139  reldmtpos  6158  mapsn  6592  mapsncnv  6597  mptelixpg  6636  elixpsn  6637  ixpsnf1o  6638  en0  6697  en1  6701  dom0  6740  exmidpw  6810  undifdcss  6819  fidcenum  6852  djuexb  6937  ctssdc  7006  exmidomni  7022  exmidfodomr  7077  elni2  7146  ltbtwnnqq  7247  enq0ref  7265  elnp1st2nd  7308  elrealeu  7661  elreal2  7662  le2tri3i  7896  elnn0nn  9043  elnnnn0b  9045  elnnnn0c  9046  elnnz  9088  elnn0z  9091  elnnz1  9101  elz2  9146  eluz2b2  9424  elnn1uz2  9428  elpqb  9468  elioo4g  9747  eluzfz2b  9844  fzm  9849  elfz1end  9866  fzass4  9873  elfz1b  9901  fz01or  9922  nn0fz0  9930  fzolb  9961  fzom  9972  elfzo0  9990  fzo1fzo0n0  9991  elfzo0z  9992  elfzo1  9998  rexanuz  10792  rexuz3  10794  sqrt0rlem  10807  fisum0diag  11242  infssuzex  11678  isprm6  11861  oddpwdclemdc  11887  ennnfone  11974  ctinfom  11977  ctinf  11979  tgclb  12273  xmetunirn  12566  bj-nnsn  13116  bdeq  13192  bdop  13244  bdunexb  13289  bj-2inf  13307  bj-nn0suc  13333  exmidsbth  13394  trirec0  13412