Theorem impbii 180

Description: Infer an equivalence from an implication and its converse. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
impbii.1	⊢ (φ → ψ)
impbii.2	⊢ (ψ → φ)

Assertion

Ref	Expression
impbii	⊢ (φ ↔ ψ)

Proof of Theorem impbii

Step	Hyp	Ref	Expression
1		impbii.1	. 2 ⊢ (φ → ψ)
2		impbii.2	. 2 ⊢ (ψ → φ)
3		bi3 179	. 2 ⊢ ((φ → ψ) → ((ψ → φ) → (φ ↔ ψ)))
4	1, 2, 3	mp2 17	1 ⊢ (φ ↔ ψ)

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  2588  r19.26  2747  ralcom3  2777  ceqsex  2894  gencbvex  2902  gencbvex2  2903  eqvinc  2967  pm13.183  2980  rr19.3v  2981  rr19.28v  2982  euxfr2  3022  reu6  3026  reu3  3027  sbnfc2  3197  sspss  3369  unineq  3506  uneqin  3507  undif3  3516  difrab  3530  compleqb  3544  un00  3587  ssdifeq0  3633  r19.2zb  3641  ralf0  3657  elpr2  3753  snidb  3760  difsnb  3851  pwpw0  3856  sssn  3865  pwsnALT  3883  unissint  3951  uniintsn  3964  iununi  4051  unipw  4118  sspwb  4119  pwadjoin  4120  preq12b  4128  pw10b  4167  pw1disj  4168  pw1exb  4327  pw1equn  4332  pw1eqadj  4333  sspw1  4336  sspw12  4337  nnc0suc  4413  lefinlteq  4464  phi11  4597  phi011  4600  opth  4603  opexb  4604  ssopab2b  4714  ssrel  4845  xpid11  4927  iss  5001  xpnz  5046  ssrnres  5060  cnveqb  5064  cnvtr  5099  cnvexb  5104  dfxp2  5114  fn0  5203  funssxp  5234  f00  5250  dffo2  5274  ffoss  5315  f1o00  5318  fo00  5319  fv3  5342  dffn5  5364  dff2  5420  dff3  5421  dffo4  5424  dffo5  5425  ffnfv  5428  fsn  5433  fsn2  5435  fconstfv  5457  isores1  5495  eqfnov2  5591  fmpt  5693  brtxp  5784  op1st2nd  5791  clos1basesuc  5883  map0  6026  mapsn  6027  ensym  6038  en0  6043  enpw1  6063  mucnc  6132  1cnc  6140  dflec3  6222  nclenc  6223  lenc  6224  ncfin  6248