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 ) )