Theorem sbanOLD

Description: Obsolete version of sban as of 13-Aug-2023. Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	sbanOLD	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ∧ 𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		sbn	⊢ ( [ 𝑦 / 𝑥 ] ¬ ( 𝜑 → ¬ 𝜓 ) ↔ ¬ [ 𝑦 / 𝑥 ] ( 𝜑 → ¬ 𝜓 ) )
2		sbim	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → ¬ 𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] ¬ 𝜓 ) )
3		sbn	⊢ ( [ 𝑦 / 𝑥 ] ¬ 𝜓 ↔ ¬ [ 𝑦 / 𝑥 ] 𝜓 )
4	3	imbi2i	⊢ ( ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] ¬ 𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 → ¬ [ 𝑦 / 𝑥 ] 𝜓 ) )
5	2 4	bitri	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → ¬ 𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 → ¬ [ 𝑦 / 𝑥 ] 𝜓 ) )
6	1 5	xchbinx	⊢ ( [ 𝑦 / 𝑥 ] ¬ ( 𝜑 → ¬ 𝜓 ) ↔ ¬ ( [ 𝑦 / 𝑥 ] 𝜑 → ¬ [ 𝑦 / 𝑥 ] 𝜓 ) )
7		df-an	⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ¬ ( 𝜑 → ¬ 𝜓 ) )
8	7	sbbii	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ∧ 𝜓 ) ↔ [ 𝑦 / 𝑥 ] ¬ ( 𝜑 → ¬ 𝜓 ) )
9		df-an	⊢ ( ( [ 𝑦 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ¬ ( [ 𝑦 / 𝑥 ] 𝜑 → ¬ [ 𝑦 / 𝑥 ] 𝜓 ) )
10	6 8 9	3bitr4i	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ∧ 𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) )