Metamath Proof Explorer

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	$⊢ φ \to (A R B \lor A = B)$
	Assertion	frege114d	$⊢ φ \to (A R B \lor A = B \lor B R A)$

Proof

Step	Hyp	Ref	Expression
1		frege114d.ab	$⊢ φ \to (A R B \lor A = B)$
2		df-3or	$⊢ (A R B \lor A = B \lor B R A) \leftrightarrow ((A R B \lor A = B) \lor B R A)$
3	2	biimpri	$⊢ ((A R B \lor A = B) \lor B R A) \to (A R B \lor A = B \lor B R A)$
4	3	orcs	$⊢ (A R B \lor A = B) \to (A R B \lor A = B \lor B R A)$
5	1 4	syl	$⊢ φ \to (A R B \lor A = B \lor B R A)$