Theorem true-P2.14 156

Description: '⊤' is a theorem.

Assertion

Ref	Expression
true-P2.14	⊢ ⊤

Proof of Theorem true-P2.14

Step	Hyp	Ref	Expression
1		id-P1.4 36	. 2 ⊢ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)
2		df-true-D2.4 155	. . 3 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
3	2	birev-P2.5b.SH 116	. 2 ⊢ ((∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥) → ⊤)
4	1, 3	ax-MP 14	1 ⊢ ⊤

Syntax hints:  term-obj 1   = wff-equals 6  ∀wff-forall 8   → wff-imp 10  ⊤wff-true 153

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14

This theorem depends on definitions:  df-bi-D2.1 107  df-true-D2.4 155

This theorem is referenced by:  false-P2.15  159  ndtruee-P3.18  183