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

Metamath Proof Explorer

Theorem 2ex2rexrot

Description: Rotate two existential quantifiers and two restricted existential quantifiers. (Contributed by AV, 9-Nov-2023)

Ref Expression
Assertion 2ex2rexrot 
|- ( E. x E. y E. z e. A E. w e. B ph <-> E. z e. A E. w e. B E. x E. y ph )

Proof

Step Hyp Ref Expression
1 rexcom4 
 |-  ( E. w e. B E. x E. y ph <-> E. x E. w e. B E. y ph )
2 1 rexbii 
 |-  ( E. z e. A E. w e. B E. x E. y ph <-> E. z e. A E. x E. w e. B E. y ph )
3 rexcom4 
 |-  ( E. z e. A E. x E. w e. B E. y ph <-> E. x E. z e. A E. w e. B E. y ph )
4 rexcom4 
 |-  ( E. w e. B E. y ph <-> E. y E. w e. B ph )
5 4 rexbii 
 |-  ( E. z e. A E. w e. B E. y ph <-> E. z e. A E. y E. w e. B ph )
6 rexcom4 
 |-  ( E. z e. A E. y E. w e. B ph <-> E. y E. z e. A E. w e. B ph )
7 5 6 bitri 
 |-  ( E. z e. A E. w e. B E. y ph <-> E. y E. z e. A E. w e. B ph )
8 7 exbii 
 |-  ( E. x E. z e. A E. w e. B E. y ph <-> E. x E. y E. z e. A E. w e. B ph )
9 2 3 8 3bitrri 
 |-  ( E. x E. y E. z e. A E. w e. B ph <-> E. z e. A E. w e. B E. x E. y ph )