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

Theorem 2th 242
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 190 1  |-  ( ph  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187
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 188
This theorem is referenced by:  2false  351  trujust  1439  dftru2  1445  bitru  1449  vjust  3081  dfnul2  3763  dfnul3  3764  rab0  3783  pwv  4218  int0  4269  0iin  4357  snnex  6611  orduninsuc  6684  fo1st  6827  fo2nd  6828  1st2val  6833  2nd2val  6834  eqer  7407  ener  7626  ruv  8124  acncc  8877  grothac  9262  grothtsk  9267  hashneq0  12551  rexfiuz  13410  foo3  28094  signswch  29458  dfpo2  30402  domep  30446  fobigcup  30672  elhf2  30947  limsucncmpi  31110  bj-vjust  31371  bj-df-v  31587  uunT1  37140  nabctnabc  38390  clifte  38394  cliftet  38395  clifteta  38396  cliftetb  38397  confun5  38402  pldofph  38404  lco0  39841
  Copyright terms: Public domain W3C validator