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

Metamath Proof Explorer

Theorem 2uasban

Description: Distribute the unabbreviated form of proper substitution in and out of a conjunction. (Contributed by Alan Sare, 31-May-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 2uasban ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 biid ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )
2 1 2uasbanh ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )