Metamath Proof Explorer


Theorem ralcom3OLD

Description: Obsolete version of ralcom3 as of 22-Dec-2024. (Contributed by NM, 22-Feb-2004) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ralcom3OLD
|- ( A. x e. A ( x e. B -> ph ) <-> A. x e. B ( x e. A -> ph ) )

Proof

Step Hyp Ref Expression
1 pm2.04
 |-  ( ( x e. A -> ( x e. B -> ph ) ) -> ( x e. B -> ( x e. A -> ph ) ) )
2 1 ralimi2
 |-  ( A. x e. A ( x e. B -> ph ) -> A. x e. B ( x e. A -> ph ) )
3 pm2.04
 |-  ( ( x e. B -> ( x e. A -> ph ) ) -> ( x e. A -> ( x e. B -> ph ) ) )
4 3 ralimi2
 |-  ( A. x e. B ( x e. A -> ph ) -> A. x e. A ( x e. B -> ph ) )
5 2 4 impbii
 |-  ( A. x e. A ( x e. B -> ph ) <-> A. x e. B ( x e. A -> ph ) )