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

Metamath Proof Explorer

Theorem sbbi

Description: Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993)

Ref Expression
Assertion sbbi 
|- ( [ y / x ] ( ph <-> ps ) <-> ( [ y / x ] ph <-> [ y / x ] ps ) )

Proof

Step Hyp Ref Expression
1 dfbi2 
 |-  ( ( ph <-> ps ) <-> ( ( ph -> ps ) /\ ( ps -> ph ) ) )
2 1 sbbii 
 |-  ( [ y / x ] ( ph <-> ps ) <-> [ y / x ] ( ( ph -> ps ) /\ ( ps -> ph ) ) )
3 sbim 
 |-  ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> [ y / x ] ps ) )
4 sbim 
 |-  ( [ y / x ] ( ps -> ph ) <-> ( [ y / x ] ps -> [ y / x ] ph ) )
5 3 4 anbi12i 
 |-  ( ( [ y / x ] ( ph -> ps ) /\ [ y / x ] ( ps -> ph ) ) <-> ( ( [ y / x ] ph -> [ y / x ] ps ) /\ ( [ y / x ] ps -> [ y / x ] ph ) ) )
6 sban 
 |-  ( [ y / x ] ( ( ph -> ps ) /\ ( ps -> ph ) ) <-> ( [ y / x ] ( ph -> ps ) /\ [ y / x ] ( ps -> ph ) ) )
7 dfbi2 
 |-  ( ( [ y / x ] ph <-> [ y / x ] ps ) <-> ( ( [ y / x ] ph -> [ y / x ] ps ) /\ ( [ y / x ] ps -> [ y / x ] ph ) ) )
8 5 6 7 3bitr4i 
 |-  ( [ y / x ] ( ( ph -> ps ) /\ ( ps -> ph ) ) <-> ( [ y / x ] ph <-> [ y / x ] ps ) )
9 2 8 bitri 
 |-  ( [ y / x ] ( ph <-> ps ) <-> ( [ y / x ] ph <-> [ y / x ] ps ) )