Theorem pm10.14

Description: Theorem *10.14 in WhiteheadRussell p. 146. (Contributed by Andrew Salmon, 17-Jun-2011)

	Ref	Expression
Assertion	pm10.14	$$⊢\left(\forall x\phi \wedge \forall x\psi \right)\to \left(\left[y/x\right]\phi \wedge \left[y/x\right]\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		stdpc4	$$⊢\forall x\phi \to \left[y/x\right]\phi$$
2		stdpc4	$$⊢\forall x\psi \to \left[y/x\right]\psi$$
3	1 2	anim12i	$$⊢\left(\forall x\phi \wedge \forall x\psi \right)\to \left(\left[y/x\right]\phi \wedge \left[y/x\right]\psi \right)$$