Metamath Proof Explorer

Theorem sbor

Description: Disjunction inside and outside of a substitution are equivalent. (Contributed by NM, 29-Sep-2002)

Ref Expression
Assertion sbor ⊢ y x φ ∨ ψ ↔ y x φ ∨ y x ψ

Proof

Step Hyp Ref Expression
1 sbim ⊢ y x ¬ φ → ψ ↔ y x ¬ φ → y x ψ
2 sbn ⊢ y x ¬ φ ↔ ¬ y x φ
3 2 imbi1i ⊢ y x ¬ φ → y x ψ ↔ ¬ y x φ → y x ψ
4 1 3 bitri ⊢ y x ¬ φ → ψ ↔ ¬ y x φ → y x ψ
5 df-or ⊢ φ ∨ ψ ↔ ¬ φ → ψ
6 5 sbbii ⊢ y x φ ∨ ψ ↔ y x ¬ φ → ψ
7 df-or ⊢ y x φ ∨ y x ψ ↔ ¬ y x φ → y x ψ
8 4 6 7 3bitr4i ⊢ y x φ ∨ ψ ↔ y x φ ∨ y x ψ