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 ⊢ φ → A R B ∨ A = B
Assertion frege114d ⊢ φ → A R B ∨ A = B ∨ B R A

Proof

Step Hyp Ref Expression
1 frege114d.ab ⊢ φ → 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 ⊢ φ → A R B ∨ A = B ∨ B R A