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

Metamath Proof Explorer

Theorem 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	$⊢ [w/ x] [y/ z] φ \leftrightarrow [y/ x] [w/ z] φ$

Proof

Step	Hyp	Ref	Expression
1		sbv	$⊢ [w/ x] φ \leftrightarrow φ$
2		sbv	$⊢ [y/ z] φ \leftrightarrow φ$
3	2	sbbii	$⊢ [w/ x] [y/ z] φ \leftrightarrow [w/ x] φ$
4		sbv	$⊢ [w/ z] φ \leftrightarrow φ$
5	4	sbbii	$⊢ [y/ x] [w/ z] φ \leftrightarrow [y/ x] φ$
6		sbv	$⊢ [y/ x] φ \leftrightarrow φ$
7	5 6	bitri	$⊢ [y/ x] [w/ z] φ \leftrightarrow φ$
8	1 3 7	3bitr4i	$⊢ [w/ x] [y/ z] φ \leftrightarrow [y/ x] [w/ z] φ$