Description: Theorem *2.521 of WhiteheadRussell p. 107. Instance of pm2.521g and of pm2.521g2 . (Contributed by NM, 3-Jan-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | pm2.521 | |- ( -. ( ph -> ps ) -> ( ps -> ph ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.521g | |- ( -. ( ph -> ps ) -> ( ps -> ph ) ) |