Description: Alternate proof of orim12d which does not depend on df-an . This is an illustration of the conservativity of definitions (definitions do not permit to prove additional theorems whose statements do not contain the defined symbol). (Contributed by Wolf Lammen, 8-Aug-2022) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | orim12dALT.1 | |- ( ph -> ( ps -> ch ) ) |
|
| orim12dALT.2 | |- ( ph -> ( th -> ta ) ) |
||
| Assertion | orim12dALT | |- ( ph -> ( ( ps \/ th ) -> ( ch \/ ta ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | orim12dALT.1 | |- ( ph -> ( ps -> ch ) ) |
|
| 2 | orim12dALT.2 | |- ( ph -> ( th -> ta ) ) |
|
| 3 | pm2.53 | |- ( ( ps \/ th ) -> ( -. ps -> th ) ) |
|
| 4 | 1 | con3d | |- ( ph -> ( -. ch -> -. ps ) ) |
| 5 | 4 2 | imim12d | |- ( ph -> ( ( -. ps -> th ) -> ( -. ch -> ta ) ) ) |
| 6 | pm2.54 | |- ( ( -. ch -> ta ) -> ( ch \/ ta ) ) |
|
| 7 | 3 5 6 | syl56 | |- ( ph -> ( ( ps \/ th ) -> ( ch \/ ta ) ) ) |