Description: The case when the content of ph is identical with the content of ps and in which ph is affirmed and ps is denied does not take place. Identical to biimp . Part of Axiom 52 of Frege1879 p. 50. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | frege52aid | |- ( ( ph <-> ps ) -> ( ph -> ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-frege52a | |- ( ( ph <-> ps ) -> ( if- ( ph , T. , F. ) -> if- ( ps , T. , F. ) ) ) |
|
2 | ifpid2 | |- ( ph <-> if- ( ph , T. , F. ) ) |
|
3 | ifpid2 | |- ( ps <-> if- ( ps , T. , F. ) ) |
|
4 | 1 2 3 | 3imtr4g | |- ( ( ph <-> ps ) -> ( ph -> ps ) ) |