MPE Home 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