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

Theorem monothetic 269
 Description: Two self-implications (see id 22) are equivalent. This theorem, rather trivial in our axiomatization, is (the biconditional form of) a standard axiom for monothetic BCI logic. This is the most general theorem of which trujust 1540 is an instance. Relatedly, this would be the justification theorem if the definition of ⊤ were dftru2 1543. (Contributed by BJ, 7-Sep-2022.)
Assertion
Ref Expression
monothetic ((𝜑𝜑) ↔ (𝜓𝜓))

Proof of Theorem monothetic
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
2 id 22 . 2 (𝜓𝜓)
31, 22th 267 1 ((𝜑𝜑) ↔ (𝜓𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  trujust  1540
 Copyright terms: Public domain W3C validator