Description: The third axiom of a system called "L" but proven to be a theorem since set.mm uses a different third axiom. This is named hirst after Holly P. Hirst and Jeffry L. Hirst. Axiom A3 of Mendelson p. 35. (Contributed by Jarvin Udandy, 7-Feb-2015) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | hirstL-ax3 | |- ( ( -. ph -> -. ps ) -> ( ( -. ph -> ps ) -> ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm4.64 | |- ( ( -. ph -> ps ) <-> ( ph \/ ps ) ) |
|
| 2 | pm4.66 | |- ( ( -. ph -> -. ps ) <-> ( ph \/ -. ps ) ) |
|
| 3 | pm2.64 | |- ( ( ph \/ ps ) -> ( ( ph \/ -. ps ) -> ph ) ) |
|
| 4 | 3 | com12 | |- ( ( ph \/ -. ps ) -> ( ( ph \/ ps ) -> ph ) ) |
| 5 | 2 4 | sylbi | |- ( ( -. ph -> -. ps ) -> ( ( ph \/ ps ) -> ph ) ) |
| 6 | 1 5 | syl5bi | |- ( ( -. ph -> -. ps ) -> ( ( -. ph -> ps ) -> ph ) ) |