Metamath Proof Explorer


Theorem monothetic

Description: Two self-implications (see id ) 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 is an instance. Relatedly, this would be the justification theorem if the definition of T. were dftru2 . (Contributed by BJ, 7-Sep-2022)

Ref Expression
Assertion monothetic
|- ( ( ph -> ph ) <-> ( ps -> ps ) )

Proof

Step Hyp Ref Expression
1 id
 |-  ( ph -> ph )
2 id
 |-  ( ps -> ps )
3 1 2 2th
 |-  ( ( ph -> ph ) <-> ( ps -> ps ) )