Description: A single axiom for propositional calculus discovered by C. A. Meredith.
This axiom has 19 symbols, sans auxiliaries. See notes in merco1 . (Contributed by Anthony Hart, 7-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | merco2 | |- ( ( ( ph -> ps ) -> ( ( F. -> ch ) -> th ) ) -> ( ( th -> ph ) -> ( ta -> ( et -> ph ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | falim | |- ( F. -> ch ) |
|
| 2 | pm2.04 | |- ( ( ( ph -> ps ) -> ( ( F. -> ch ) -> th ) ) -> ( ( F. -> ch ) -> ( ( ph -> ps ) -> th ) ) ) |
|
| 3 | 1 2 | mpi | |- ( ( ( ph -> ps ) -> ( ( F. -> ch ) -> th ) ) -> ( ( ph -> ps ) -> th ) ) |
| 4 | jarl | |- ( ( ( ph -> ps ) -> th ) -> ( -. ph -> th ) ) |
|
| 5 | idd | |- ( ( ( ph -> ps ) -> th ) -> ( th -> th ) ) |
|
| 6 | 4 5 | jad | |- ( ( ( ph -> ps ) -> th ) -> ( ( ph -> th ) -> th ) ) |
| 7 | looinv | |- ( ( ( ph -> th ) -> th ) -> ( ( th -> ph ) -> ph ) ) |
|
| 8 | 3 6 7 | 3syl | |- ( ( ( ph -> ps ) -> ( ( F. -> ch ) -> th ) ) -> ( ( th -> ph ) -> ph ) ) |
| 9 | 8 | a1dd | |- ( ( ( ph -> ps ) -> ( ( F. -> ch ) -> th ) ) -> ( ( th -> ph ) -> ( ta -> ph ) ) ) |
| 10 | 9 | a1i | |- ( et -> ( ( ( ph -> ps ) -> ( ( F. -> ch ) -> th ) ) -> ( ( th -> ph ) -> ( ta -> ph ) ) ) ) |
| 11 | 10 | com4l | |- ( ( ( ph -> ps ) -> ( ( F. -> ch ) -> th ) ) -> ( ( th -> ph ) -> ( ta -> ( et -> ph ) ) ) ) |