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 yxφψyxφyxψ

Proof

Step Hyp Ref Expression
1 sbim yx¬φψyx¬φyxψ
2 sbn yx¬φ¬yxφ
3 2 imbi1i yx¬φyxψ¬yxφyxψ
4 1 3 bitri yx¬φψ¬yxφyxψ
5 df-or φψ¬φψ
6 5 sbbii yxφψyx¬φψ
7 df-or yxφyxψ¬yxφyxψ
8 4 6 7 3bitr4i yxφψyxφyxψ