Theorem truejust-P2.13 154

Description: Justification Theorem for df-true-D2.4 155.

Assertion

Ref	Expression
truejust-P2.13	⊢ ((∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥) ↔ (∀𝑦 𝑦 = 𝑦 → ∀𝑦 𝑦 = 𝑦))

Proof of Theorem truejust-P2.13

Step	Hyp	Ref	Expression
1		id-P1.4 36	. . 3 ⊢ (∀𝑦 𝑦 = 𝑦 → ∀𝑦 𝑦 = 𝑦)
2	1	axL1.SH 30	. 2 ⊢ ((∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥) → (∀𝑦 𝑦 = 𝑦 → ∀𝑦 𝑦 = 𝑦))
3		id-P1.4 36	. . 3 ⊢ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)
4	3	axL1.SH 30	. 2 ⊢ ((∀𝑦 𝑦 = 𝑦 → ∀𝑦 𝑦 = 𝑦) → (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
5	2, 4	bicmb-P2.5c.2SH 120	1 ⊢ ((∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥) ↔ (∀𝑦 𝑦 = 𝑦 → ∀𝑦 𝑦 = 𝑦))

Syntax hints:  term-obj 1   = wff-equals 6  ∀wff-forall 8   → wff-imp 10   ↔ wff-bi 104

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

This theorem is referenced by: (None)