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

Theorem 2th 230
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 10 . 2  |-  ( ph  ->  ps )
3 2th.1 . . 3  |-  ph
43a1i 10 . 2  |-  ( ps 
->  ph )
52, 4impbii 180 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  2false  339  trujust  1309  bitru  1317  pm11.07  2054  vjust  2789  dfnul2  3457  dfnul3  3458  rab0  3475  pwv  3826  int0  3876  0iin  3960  snnex  4524  orduninsuc  4634  fo1st  6139  fo2nd  6140  1st2val  6145  2nd2val  6146  eqer  6693  ener  6908  ruv  7314  acncc  8066  grothac  8452  grothtsk  8457  rexfiuz  11831  foo3  23023  dfpo2  24112  domep  24149  fobigcup  24440  elhf2  24805  limsucncmpi  24884  vutr  24950  inpc  25277  1ded  25738
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator