| Step |
Hyp |
Ref |
Expression |
| 1 |
|
orel.1 |
|- ( ( ps /\ et ) -> th ) |
| 2 |
|
orel.2 |
|- ( ( ch /\ rh ) -> th ) |
| 3 |
|
orel.3 |
|- ( ph -> ( ps \/ ch ) ) |
| 4 |
|
simprl |
|- ( ( ph /\ ( et /\ rh ) ) -> et ) |
| 5 |
1
|
ancoms |
|- ( ( et /\ ps ) -> th ) |
| 6 |
4 5
|
sylan |
|- ( ( ( ph /\ ( et /\ rh ) ) /\ ps ) -> th ) |
| 7 |
|
simprr |
|- ( ( ph /\ ( et /\ rh ) ) -> rh ) |
| 8 |
2
|
ancoms |
|- ( ( rh /\ ch ) -> th ) |
| 9 |
7 8
|
sylan |
|- ( ( ( ph /\ ( et /\ rh ) ) /\ ch ) -> th ) |
| 10 |
3
|
adantr |
|- ( ( ph /\ ( et /\ rh ) ) -> ( ps \/ ch ) ) |
| 11 |
6 9 10
|
mpjaodan |
|- ( ( ph /\ ( et /\ rh ) ) -> th ) |