Theorem 19.42vv 1907

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 1906	. 2 ⊢ (∃x∃y(φ ∧ ψ) ↔ ∃x(φ ∧ ∃yψ))
2		19.42v 1905	. 2 ⊢ (∃x(φ ∧ ∃yψ) ↔ (φ ∧ ∃x∃yψ))
3	1, 2	bitri 240	1 ⊢ (∃x∃y(φ ∧ ψ) ↔ (φ ∧ ∃x∃yψ))

Syntax hints:   ↔ wb 176   ∧ wa 358  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545

This theorem is referenced by:  19.42vvv  1908  exdistr2  1909  3exdistr  1910  ceqsex3v  2897  ceqsex4v  2898  ceqsex8v  2900  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  sikexlem  4295  insklem  4304  elswap  4740  dmsi  5519  dfoprab2  5558  resoprab  5581  ov3  5599  ov6g  5600  brpprod  5839  dmpprod  5840  lecex  6115  ce0nnul  6177