MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2th Structured version   Unicode version

Theorem 2th 239
Description: Two truths are equivalent. (Contributed by NM, 18-Aug-1993.)
Hypotheses
Ref Expression
2th.1  |-  ph
2th.2  |-  ps
Assertion
Ref Expression
2th  |-  ( ph  <->  ps )

Proof of Theorem 2th
StepHypRef Expression
1 2th.2 . . 3  |-  ps
21a1i 11 . 2  |-  ( ph  ->  ps )
3 2th.1 . . 3  |-  ph
43a1i 11 . 2  |-  ( ps 
->  ph )
52, 4impbii 188 1  |-  ( ph  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184
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 185
This theorem is referenced by:  2false  348  trujust  1407  dftru2  1413  bitru  1417  vjust  3059  dfnul2  3739  dfnul3  3740  rab0  3759  pwv  4189  int0  4240  0iin  4328  snnex  6587  orduninsuc  6660  fo1st  6803  fo2nd  6804  1st2val  6809  2nd2val  6810  eqer  7380  ener  7599  ruv  8059  acncc  8851  grothac  9237  grothtsk  9242  hashneq0  12480  rexfiuz  13327  foo3  27761  signswch  29010  dfpo2  29955  domep  29999  fobigcup  30225  elhf2  30500  limsucncmpi  30664  bj-vjust  30923  bj-df-v  31135  uunT1  36581  lco0  38520
  Copyright terms: Public domain W3C validator