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	|- ( ph -> ( A R B \/ A = B ) )
Assertion	frege114d	|- ( ph -> ( A R B \/ A = B \/ B R A ) )

Proof

Step	Hyp	Ref	Expression
1		frege114d.ab	|- ( ph -> ( A R B \/ A = B ) )
2		df-3or	|- ( ( A R B \/ A = B \/ B R A ) <-> ( ( A R B \/ A = B ) \/ B R A ) )
3	2	biimpri	|- ( ( ( A R B \/ A = B ) \/ B R A ) -> ( A R B \/ A = B \/ B R A ) )
4	3	orcs	|- ( ( A R B \/ A = B ) -> ( A R B \/ A = B \/ B R A ) )
5	1 4	syl	|- ( ph -> ( A R B \/ A = B \/ B R A ) )