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  exiftru  1647  pm11.07  2067  vjust  2802  dfnul2  3470  dfnul3  3471  rab0  3488  pwv  3842  int0  3892  0iin  3976  snnex  4540  orduninsuc  4650  fo1st  6155  fo2nd  6156  1st2val  6161  2nd2val  6162  eqer  6709  ener  6924  ruv  7330  acncc  8082  grothac  8468  grothtsk  8473  rexfiuz  11847  foo3  23039  dfpo2  24183  domep  24220  fobigcup  24511  elhf2  24877  limsucncmpi  24956  vutr  25053  inpc  25380  1ded  25841  pm11.07OLD7  29716
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