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  1381  dftru2  1387  bitru  1391  vjust  3114  dfnul2  3787  dfnul3  3788  rab0  3806  pwv  4244  int0  4296  0iin  4383  snnex  6584  orduninsuc  6656  fo1st  6801  fo2nd  6802  1st2val  6807  2nd2val  6808  eqer  7341  ener  7559  ruv  8023  acncc  8816  grothac  9204  grothtsk  9209  hashneq0  12396  rexfiuz  13136  foo3  27035  signswch  28155  dfpo2  28758  domep  28799  fobigcup  29124  elhf2  29406  limsucncmpi  29484  lco0  32101  uunT1  32657  bj-vjust  33453  bj-df-v  33664
  Copyright terms: Public domain W3C validator