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

Theorem 2th 266
 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 211 1 (𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 208 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 209 This theorem is referenced by:  monothetic  268  2false  378  dftru2  1536  bitru  1540  vjust  3494  dfnul2OLD  4292  dfnul3  4293  pwv  4827  int0  4881  0iin  4978  domepOLD  5787  orduninsuc  7550  fo1st  7701  fo2nd  7702  1st2val  7709  2nd2val  7710  eqer  8316  ener  8548  ruv  9058  acncc  9854  grothac  10244  grothtsk  10249  hashneq0  13717  rexfiuz  14699  sa-abvi  30212  signswch  31824  satfdm  32609  dfpo2  32984  fobigcup  33354  elhf2  33629  limsucncmpi  33786  bj-df-v  34339  uunT1  41105  nabctnabc  43158  clifte  43162  cliftet  43163  clifteta  43164  cliftetb  43165  confun5  43170  pldofph  43172  lco0  44473  line2ylem  44729
 Copyright terms: Public domain W3C validator