Description: Theorem *11.62 in WhiteheadRussell p. 166. Importation combined with the rearrangement with quantifiers. (Contributed by Andrew Salmon, 24-May-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | pm11.62 | |- ( A. x A. y ( ( ph /\ ps ) -> ch ) <-> A. x ( ph -> A. y ( ps -> ch ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | impexp | |- ( ( ( ph /\ ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) |
|
2 | 1 | albii | |- ( A. y ( ( ph /\ ps ) -> ch ) <-> A. y ( ph -> ( ps -> ch ) ) ) |
3 | 19.21v | |- ( A. y ( ph -> ( ps -> ch ) ) <-> ( ph -> A. y ( ps -> ch ) ) ) |
|
4 | 2 3 | bitri | |- ( A. y ( ( ph /\ ps ) -> ch ) <-> ( ph -> A. y ( ps -> ch ) ) ) |
5 | 4 | albii | |- ( A. x A. y ( ( ph /\ ps ) -> ch ) <-> A. x ( ph -> A. y ( ps -> ch ) ) ) |