Description: If there is a choice only between ph and ph , then ph takes place. Identical to pm2.18 . Proposition 43 of Frege1879 p. 47. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | frege43 | |- ( ( -. ph -> ph ) -> ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | frege42 | |- -. -. ( ph -> ph ) |
|
| 2 | frege40 | |- ( -. -. ( ph -> ph ) -> ( ( -. ph -> ph ) -> ph ) ) |
|
| 3 | 1 2 | ax-mp | |- ( ( -. ph -> ph ) -> ph ) |