Theorem sbco2d
A composition law for substitution. Usage of this theorem is
discouraged because it depends on [ax-13]. (Contributed by NM,
2-Jun-1993.) (Revised by Mario Carneiro, 6-Oct-2016.)
(New usage is discouraged.)
Hypotheses
sbco2d.1
\( \vdash \Finv x \, \varphi \)
sbco2d.2
\( \vdash \Finv z \, \varphi \)
sbco2d.3
\( \vdash \varphi \rightarrow \Finv z \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow ([ y' / z ] \, [ z / x ] \, \psi \leftrightarrow [ y' / x ] \, \psi) \)
Proof
l0
sbco2d.2
sbco2d.3
nfim1 l0 _
l3
sbco2 _
\( \vdash [ y' / z ] \, [ z / x ] \, (\varphi \rightarrow \psi) \leftrightarrow [ y' / x ] \, (\varphi \rightarrow \psi) \)
sbco2d.1
sbrim _
l6
sbbii _
\( \vdash [ y' / z ] \, [ z / x ] \, (\varphi \rightarrow \psi) \leftrightarrow [ y' / z ] \, (\varphi \rightarrow [ z / x ] \, \psi) \)
sbco2d.2
sbrim _
\( \vdash [ y' / z ] \, (\varphi \rightarrow [ z / x ] \, \psi) \leftrightarrow \varphi \rightarrow [ y' / z ] \, [ z / x ] \, \psi \)
l9
bitri l6 _
\( \vdash [ y' / z ] \, [ z / x ] \, (\varphi \rightarrow \psi) \leftrightarrow \varphi \rightarrow [ y' / z ] \, [ z / x ] \, \psi \)
sbco2d.1
sbrim _
\( \vdash [ y' / x ] \, (\varphi \rightarrow \psi) \leftrightarrow \varphi \rightarrow [ y' / x ] \, \psi \)
3bitr3i l3 l9 _
pm5.74ri _