Theorem elimhyps2

Description: Generalization of elimhyps that is not useful unless we can separately prove |- A e. _V . (Contributed by NM, 13-Jun-2019)

	Ref	Expression
Hypothesis	elimhyps2.1	⊢ [ 𝐵 / 𝑥 ] 𝜑
Assertion	elimhyps2	⊢ [ if ( [ 𝐴 / 𝑥 ] 𝜑 , 𝐴 , 𝐵 ) / 𝑥 ] 𝜑

Proof

Step	Hyp	Ref	Expression
1		elimhyps2.1	⊢ [ 𝐵 / 𝑥 ] 𝜑
2		dfsbcq	⊢ ( 𝐴 = if ( [ 𝐴 / 𝑥 ] 𝜑 , 𝐴 , 𝐵 ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ if ( [ 𝐴 / 𝑥 ] 𝜑 , 𝐴 , 𝐵 ) / 𝑥 ] 𝜑 ) )
3		dfsbcq	⊢ ( 𝐵 = if ( [ 𝐴 / 𝑥 ] 𝜑 , 𝐴 , 𝐵 ) → ( [ 𝐵 / 𝑥 ] 𝜑 ↔ [ if ( [ 𝐴 / 𝑥 ] 𝜑 , 𝐴 , 𝐵 ) / 𝑥 ] 𝜑 ) )
4	2 3 1	elimhyp	⊢ [ if ( [ 𝐴 / 𝑥 ] 𝜑 , 𝐴 , 𝐵 ) / 𝑥 ] 𝜑