Theorem sbievw2
sbievw applied twice, avoiding a DV condition on \( x \), \( y' \).
Based on proofs by Wolf Lammen. (Contributed by Steven Nguyen,
29-Jul-2023.)
Hypotheses
sbievw2.1
\( \vdash x = w \rightarrow (\varphi \leftrightarrow \chi) \)
sbievw2.2
\( \vdash w = y' \rightarrow (\chi \leftrightarrow \psi) \)
Conclusion
\( \vdash [ y' / x ] \, \varphi \leftrightarrow \psi \)
Proof
l0
sbcom3vv
\( \vdash [ y' / w ] \, [ w / x ] \, \varphi \leftrightarrow [ y' / w ] \, [ y' / x ] \, \varphi \)
sbievw2.1
sbievw _
l3
sbbii _
\( \vdash [ y' / w ] \, [ w / x ] \, \varphi \leftrightarrow [ y' / w ] \, \chi \)
sbv
\( \vdash [ y' / w ] \, [ y' / x ] \, \varphi \leftrightarrow [ y' / x ] \, \varphi \)
l5
3bitr3i l0 l3 _
\( \vdash [ y' / w ] \, \chi \leftrightarrow [ y' / x ] \, \varphi \)
sbievw2.2
sbievw _
\( \vdash [ y' / w ] \, \chi \leftrightarrow \psi \)
bitr3i l5 _