Theorem impbii 180

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  dfbi1  184  bicom  191  biid  227  2th  230  pm5.74  235  bitri  240  notnot  282  con34b  283  notbi  286  bibi2i  304  con1b  323  con2b  324  bi2.04  350  pm5.4  351  imdi  352  pm4.8  354  pm4.81  355  orcom  376  dfor2  400  impexp  433  ancom  437  oridm  500  orbi2i  505  or12  509  pm4.45im  545  pm4.44  560  pm4.79  566  anass  630  jaob  758  jcab  833  andi  837  pm4.72  846  oibabs  851  pm4.82  894  consensus  925  rnlem  931  3jaob  1244  truan  1331  dfnot  1332  3impexp  1366  3impexpbicom  1367  cad1  1398  tbw-bijust  1463  tbw-negdf  1464  19.26  1593  sbbii  1653  19.9v  1664  equcom  1680  ax12b  1689  19.3vOLD  1696  cbvalw  1701  cbvalvw  1702  alcom  1737  19.9hOLD  1781  19.3  1785  19.23hOLD  1820  equsalhwOLD  1839  19.21hOLD  1840  excomOLD  1859  19.41  1879  ax12olem1  1927  ax12olem3  1929  equsal  1960  cbval  1984  equs45f  1989  equvin  2001  sb6f  2039  dfsb2  2055  sbn  2062  sbim  2065  sb5rf  2090  sb6rf  2091  sb8  2092  sb9  2095  mo  2226  eu2  2229  mo2  2233  exmoeu  2246  euan  2261  2mo  2282  2eu6  2289  axext4  2337  cleqh  2450  nebi  2587  r19.26  2746  ralcom3  2776  ceqsex  2893  gencbvex  2901  gencbvex2  2902  eqvinc  2966  pm13.183  2979  rr19.3v  2980  rr19.28v  2981  euxfr2  3021  reu6  3025  reu3  3026  sbnfc2  3196  sspss  3368  unineq  3505  uneqin  3506  undif3  3515  difrab  3529  compleqb  3543  un00  3586  ssdifeq0  3632  r19.2zb  3640  ralf0  3656  elpr2  3752  snidb  3759  difsnb  3850  pwpw0  3855  sssn  3864  pwsnALT  3882  unissint  3950  uniintsn  3963  iununi  4050  unipw  4117  sspwb  4118  pwadjoin  4119  preq12b  4127  pw10b  4166  pw1disj  4167  pw1exb  4326  pw1equn  4331  pw1eqadj  4332  sspw1  4335  sspw12  4336  nnc0suc  4412  lefinlteq  4463  phi11  4596  phi011  4599  opth  4602  opexb  4603  ssopab2b  4713  ssrel  4844  xpid11  4926  iss  5000  xpnz  5045  ssrnres  5059  cnveqb  5063  cnvtr  5098  cnvexb  5103  dfxp2  5113  fn0  5202  funssxp  5233  f00  5249  dffo2  5273  ffoss  5314  f1o00  5317  fo00  5318  fv3  5341  dffn5  5363  dff2  5419  dff3  5420  dffo4  5423  dffo5  5424  ffnfv  5427  fsn  5432  fsn2  5434  fconstfv  5456  isores1  5494  eqfnov2  5590  fmpt  5692  brtxp  5783  op1st2nd  5790  clos1basesuc  5882  map0  6025  mapsn  6026  ensym  6037  en0  6042  enpw1  6062  mucnc  6131  1cnc  6139  dflec3  6221  nclenc  6222  lenc  6223  ncfin  6247