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  350  trujust  1372  dftru2  1378  bitru  1382  vjust  3073  dfnul2  3742  dfnul3  3743  rab0  3761  pwv  4193  int0  4245  0iin  4331  snnex  6487  orduninsuc  6559  fo1st  6701  fo2nd  6702  1st2val  6707  2nd2val  6708  eqer  7239  ener  7461  ruv  7922  acncc  8715  grothac  9103  grothtsk  9108  hashneq0  12244  rexfiuz  12948  foo3  25994  signswch  27101  dfpo2  27704  domep  27745  fobigcup  28070  elhf2  28352  limsucncmpi  28430  lco0  31075  uunT1  31826  bj-vjust  32620  bj-df-v  32831
  Copyright terms: Public domain W3C validator