This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ] ( ph \/ ps ) <-> ( [ y / x ] ph \/ [ y / x ] ps ) )

Proof

Step Hyp Ref Expression
1 sbim 
 |-  ( [ y / x ] ( -. ph -> ps ) <-> ( [ y / x ] -. ph -> [ y / x ] ps ) )
2 sbn 
 |-  ( [ y / x ] -. ph <-> -. [ y / x ] ph )
3 2 imbi1i 
 |-  ( ( [ y / x ] -. ph -> [ y / x ] ps ) <-> ( -. [ y / x ] ph -> [ y / x ] ps ) )
4 1 3 bitri 
 |-  ( [ y / x ] ( -. ph -> ps ) <-> ( -. [ y / x ] ph -> [ y / x ] ps ) )
5 df-or 
 |-  ( ( ph \/ ps ) <-> ( -. ph -> ps ) )
6 5 sbbii 
 |-  ( [ y / x ] ( ph \/ ps ) <-> [ y / x ] ( -. ph -> ps ) )
7 df-or 
 |-  ( ( [ y / x ] ph \/ [ y / x ] ps ) <-> ( -. [ y / x ] ph -> [ y / x ] ps ) )
8 4 6 7 3bitr4i 
 |-  ( [ y / x ] ( ph \/ ps ) <-> ( [ y / x ] ph \/ [ y / x ] ps ) )