Theorem 19.42vv 1785

Description: Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 16-Mar-1995.)

Assertion

Ref	Expression
19.42vv	⊢ (∃x∃y(φ ∧ ψ) ↔ (φ ∧ ∃x∃yψ))

Distinct variable groups:   φ,x   φ,y

Allowed substitution hints:   ψ(x,y)

Proof of Theorem 19.42vv

Step	Hyp	Ref	Expression
1		exdistr 1784	. 2 ⊢ (∃x∃y(φ ∧ ψ) ↔ ∃x(φ ∧ ∃yψ))
2		19.42v 1783	. 2 ⊢ (∃x(φ ∧ ∃yψ) ↔ (φ ∧ ∃x∃yψ))
3	1, 2	bitri 173	1 ⊢ (∃x∃y(φ ∧ ψ) ↔ (φ ∧ ∃x∃yψ))

Syntax hints:   ∧ wa 97   ↔ wb 98  ∃wex 1378

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  19.42vvv  1786  19.42vvvv  1787  exdistr2  1788  3exdistr  1789  ceqsex3v  2590  ceqsex4v  2591  elvvv  4346  dfoprab2  5494  resoprab  5539  ovi3  5579  ov6g  5580  oprabex3  5698  xpassen  6240  enq0enq  6414  enq0sym  6415  nqnq0pi  6421