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

Theorem 2th 231
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 181 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  2false  340  trujust  1324  bitru  1332  exiftruOLD  1665  pm11.07OLD  2151  vjust  2902  dfnul2  3575  dfnul3  3576  rab0  3593  pwv  3958  int0  4008  0iin  4092  snnex  4655  orduninsuc  4765  fo1st  6307  fo2nd  6308  1st2val  6313  2nd2val  6314  eqer  6876  ener  7092  ruv  7503  acncc  8255  grothac  8640  grothtsk  8645  rexfiuz  12080  foo3  23796  dfpo2  25138  domep  25175  fobigcup  25466  elhf2  25832  limsucncmpi  25911
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 178
  Copyright terms: Public domain W3C validator