Description: Swap antecedents. Theorem *2.04 of WhiteheadRussell p. 100. This was the third axiom in Frege's logic system, specifically Proposition 8 of Frege1879 p. 35. Copy of pm2.04 with a different proof. (Contributed by Wolf Lammen, 7-Jul-2019) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-luk-pm2.04 | |- ( ( ph -> ( ps -> ch ) ) -> ( ps -> ( ph -> ch ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wl-luk-ax1 | |- ( ps -> ( ph -> ps ) ) |
|
| 2 | wl-luk-ax2 | |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) |
|
| 3 | 1 2 | wl-luk-imtrid | |- ( ( ph -> ( ps -> ch ) ) -> ( ps -> ( ph -> ch ) ) ) |