Metamath Proof Explorer
Description: Theorem *13.18 in WhiteheadRussell p. 178. (Contributed by Andrew
Salmon, 3-Jun-2011) (Proof shortened by Wolf Lammen, 14-May-2023)
|
|
Ref |
Expression |
|
Assertion |
pm13.18 |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
neeq1 |
|
2 |
1
|
biimpd |
|
3 |
2
|
imp |
|