This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ ( ( 𝜑 → 𝜑 ) ↔ ( 𝜓 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝜑 → 𝜑 )
2		id	⊢ ( 𝜓 → 𝜓 )
3	1 2	2th	⊢ ( ( 𝜑 → 𝜑 ) ↔ ( 𝜓 → 𝜓 ) )