Metamath Proof Explorer

Theorem pm11.6

Description: Theorem *11.6 in WhiteheadRussell p. 165. (Contributed by Andrew Salmon, 25-May-2011)

Ref Expression
Assertion pm11.6 
|- ( E. x ( E. y ( ph /\ ps ) /\ ch ) <-> E. y ( E. x ( ph /\ ch ) /\ ps ) )

Proof

Step Hyp Ref Expression
1 excom 
 |-  ( E. x E. y ( ( ph /\ ps ) /\ ch ) <-> E. y E. x ( ( ph /\ ps ) /\ ch ) )
2 an32 
 |-  ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ph /\ ch ) /\ ps ) )
3 2 2exbii 
 |-  ( E. y E. x ( ( ph /\ ps ) /\ ch ) <-> E. y E. x ( ( ph /\ ch ) /\ ps ) )
4 1 3 bitri 
 |-  ( E. x E. y ( ( ph /\ ps ) /\ ch ) <-> E. y E. x ( ( ph /\ ch ) /\ ps ) )
5 19.41v 
 |-  ( E. y ( ( ph /\ ps ) /\ ch ) <-> ( E. y ( ph /\ ps ) /\ ch ) )
6 5 exbii 
 |-  ( E. x E. y ( ( ph /\ ps ) /\ ch ) <-> E. x ( E. y ( ph /\ ps ) /\ ch ) )
7 19.41v 
 |-  ( E. x ( ( ph /\ ch ) /\ ps ) <-> ( E. x ( ph /\ ch ) /\ ps ) )
8 7 exbii 
 |-  ( E. y E. x ( ( ph /\ ch ) /\ ps ) <-> E. y ( E. x ( ph /\ ch ) /\ ps ) )
9 4 6 8 3bitr3i 
 |-  ( E. x ( E. y ( ph /\ ps ) /\ ch ) <-> E. y ( E. x ( ph /\ ch ) /\ ps ) )