MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2th Structured version   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  1327  bitru  1335  exiftruOLD  1670  pm11.07OLD  2191  vjust  2949  dfnul2  3622  dfnul3  3623  rab0  3640  pwv  4006  int0  4056  0iin  4141  snnex  4705  orduninsuc  4815  fo1st  6358  fo2nd  6359  1st2val  6364  2nd2val  6365  eqer  6930  ener  7146  ruv  7560  acncc  8312  grothac  8697  grothtsk  8702  rexfiuz  12143  foo3  23938  dfpo2  25370  domep  25412  fobigcup  25737  elhf2  26108  limsucncmpi  26187
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