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

Theorem 2th 254
Description: Two truths are equivalent. (Contributed by NM, 18-Aug-1993.)
Hypotheses
Ref Expression
2th.1 𝜑
2th.2 𝜓
Assertion
Ref Expression
2th (𝜑𝜓)

Proof of Theorem 2th
StepHypRef Expression
1 2th.2 . . 3 𝜓
21a1i 11 . 2 (𝜑𝜓)
3 2th.1 . . 3 𝜑
43a1i 11 . 2 (𝜓𝜑)
52, 4impbii 199 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196
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 197
This theorem is referenced by:  2false  364  trujust  1632  dftru2  1638  bitru  1643  vjust  3339  dfnul2  4058  dfnul3  4059  rab0OLD  4097  pwv  4583  int0  4640  int0OLD  4641  0iin  4728  snnexOLD  7130  orduninsuc  7206  fo1st  7351  fo2nd  7352  1st2val  7359  2nd2val  7360  eqer  7944  ener  8166  ruv  8670  acncc  9452  grothac  9842  grothtsk  9847  hashneq0  13345  rexfiuz  14284  foo3  29609  signswch  30945  dfpo2  31950  domep  32001  fobigcup  32311  elhf2  32586  limsucncmpi  32748  bj-vjust  33090  bj-df-v  33320  uunT1  39507  nabctnabc  41602  clifte  41606  cliftet  41607  clifteta  41608  cliftetb  41609  confun5  41614  pldofph  41616  lco0  42724
  Copyright terms: Public domain W3C validator