Metamath Proof Explorer
Description: Inference adding two existential quantifiers to both sides of an
equivalence. (Contributed by NM, 16Mar1995)


Ref 
Expression 

Hypothesis 
2exbii.1 
⊢ ( 𝜑 ↔ 𝜓 ) 

Assertion 
2exbii 
⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 𝜓 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

2exbii.1 
⊢ ( 𝜑 ↔ 𝜓 ) 
2 
1

exbii 
⊢ ( ∃ 𝑦 𝜑 ↔ ∃ 𝑦 𝜓 ) 
3 
2

exbii 
⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 𝜓 ) 