Theorem frege114d

Description: If either R relates A and B or A and B are the same, then either A and B are the same, R relates A and B , R relates B and A . Similar to Proposition 114 of Frege1879 p. 76. Compare with frege114 . (Contributed by RP, 15-Jul-2020)

	Ref	Expression
Hypothesis	frege114d.ab	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ∨ 𝐴 = 𝐵 ) )
Assertion	frege114d	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 𝑅 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		frege114d.ab	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ∨ 𝐴 = 𝐵 ) )
2		df-3or	⊢ ( ( 𝐴 𝑅 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 𝑅 𝐴 ) ↔ ( ( 𝐴 𝑅 𝐵 ∨ 𝐴 = 𝐵 ) ∨ 𝐵 𝑅 𝐴 ) )
3	2	biimpri	⊢ ( ( ( 𝐴 𝑅 𝐵 ∨ 𝐴 = 𝐵 ) ∨ 𝐵 𝑅 𝐴 ) → ( 𝐴 𝑅 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 𝑅 𝐴 ) )
4	3	orcs	⊢ ( ( 𝐴 𝑅 𝐵 ∨ 𝐴 = 𝐵 ) → ( 𝐴 𝑅 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 𝑅 𝐴 ) )
5	1 4	syl	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 𝑅 𝐴 ) )