Step |
Hyp |
Ref |
Expression |
1 |
|
con3 |
|- ( ( ph -> ps ) -> ( -. ps -> -. ph ) ) |
2 |
1
|
orim1d |
|- ( ( ph -> ps ) -> ( ( -. ps \/ -. ch ) -> ( -. ph \/ -. ch ) ) ) |
3 |
|
pm3.13 |
|- ( -. ( ps /\ ch ) -> ( -. ps \/ -. ch ) ) |
4 |
|
pm3.14 |
|- ( ( -. ph \/ -. ch ) -> -. ( ph /\ ch ) ) |
5 |
3 4
|
imim12i |
|- ( ( ( -. ps \/ -. ch ) -> ( -. ph \/ -. ch ) ) -> ( -. ( ps /\ ch ) -> -. ( ph /\ ch ) ) ) |
6 |
|
df-nan |
|- ( ( ps -/\ ch ) <-> -. ( ps /\ ch ) ) |
7 |
|
df-nan |
|- ( ( ph -/\ ch ) <-> -. ( ph /\ ch ) ) |
8 |
5 6 7
|
3imtr4g |
|- ( ( ( -. ps \/ -. ch ) -> ( -. ph \/ -. ch ) ) -> ( ( ps -/\ ch ) -> ( ph -/\ ch ) ) ) |
9 |
2 8
|
syl |
|- ( ( ph -> ps ) -> ( ( ps -/\ ch ) -> ( ph -/\ ch ) ) ) |