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 ⊢ ∃ x ∃ y x = u ∧ y = v ∧ φ ∧ ψ ↔ ∃ x ∃ y x = u ∧ y = v ∧ φ ∧ ∃ x ∃ y x = u ∧ y = v ∧ ψ

Proof

Step Hyp Ref Expression
1 biid ⊢ ∃ x ∃ y x = u ∧ y = v ∧ φ ∧ ∃ x ∃ y x = u ∧ y = v ∧ ψ ↔ ∃ x ∃ y x = u ∧ y = v ∧ φ ∧ ∃ x ∃ y x = u ∧ y = v ∧ ψ
2 1 2uasbanh ⊢ ∃ x ∃ y x = u ∧ y = v ∧ φ ∧ ψ ↔ ∃ x ∃ y x = u ∧ y = v ∧ φ ∧ ∃ x ∃ y x = u ∧ y = v ∧ ψ