# Metamath Proof Explorer

## Theorem hbra2VD

Description: Virtual deduction proof of nfra2 . The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

 1:: |- ( A. y e. B A. x e. A ph -> A. y A. y e. B A. x e. A ph ) 2:: |- ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph ) 3:1,2,?: e00 |- ( A. x e. A A. y e. B ph -> A. y A. y e. B A. x e. A ph ) 4:2: |- A. y ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph ) 5:4,?: e0a |- ( A. y A. x e. A A. y e. B ph <-> A. y A. y e. B A. x e. A ph ) qed:3,5,?: e00 |- ( A. x e. A A. y e. B ph -> A. y A. x e. A A. y e. B ph )
(Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion hbra2VD ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 ralcom ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
2 hbra1 ${⊢}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
3 1 2 hbxfrbi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }$