Description: Version of 19.42 with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993)
Ref | Expression | ||
---|---|---|---|
Assertion | 19.42v | |- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.41v | |- ( E. x ( ps /\ ph ) <-> ( E. x ps /\ ph ) ) |
|
2 | exancom | |- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) ) |
|
3 | ancom | |- ( ( ph /\ E. x ps ) <-> ( E. x ps /\ ph ) ) |
|
4 | 1 2 3 | 3bitr4i | |- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) ) |