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 x A x B φ x B x A φ

Proof

Step Hyp Ref Expression
1 pm2.04 x A x B φ x B x A φ
2 1 ralimi2 x A x B φ x B x A φ
3 pm2.04 x B x A φ x A x B φ
4 3 ralimi2 x B x A φ x A x B φ
5 2 4 impbii x A x B φ x B x A φ