This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes) Define proper substitution sbcom4
Description: Commutativity law for substitution. This theorem was incorrectly used
as our previous version of pm11.07 but may still be useful.
(Contributed by Andrew Salmon , 17-Jun-2011) (Proof shortened by Jim
Kingdon , 22-Jan-2018)
Ref
Expression
Assertion
sbcom4 ⊢ ( [ 𝑤 / 𝑥 ] [ 𝑦 / 𝑧 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 )
Proof
Step
Hyp
Ref
Expression
1
sbv ⊢ ( [ 𝑤 / 𝑥 ] 𝜑 ↔ 𝜑 )
2
sbv ⊢ ( [ 𝑦 / 𝑧 ] 𝜑 ↔ 𝜑 )
3
2
sbbii ⊢ ( [ 𝑤 / 𝑥 ] [ 𝑦 / 𝑧 ] 𝜑 ↔ [ 𝑤 / 𝑥 ] 𝜑 )
4
sbv ⊢ ( [ 𝑤 / 𝑧 ] 𝜑 ↔ 𝜑 )
5
4
sbbii ⊢ ( [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 )
6
sbv ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 )
7
5 6
bitri ⊢ ( [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 ↔ 𝜑 )
8
1 3 7
3bitr4i ⊢ ( [ 𝑤 / 𝑥 ] [ 𝑦 / 𝑧 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 )