This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Inference associated with pm2.24 . Its associated inference is
pm2.24ii . (Contributed by NM, 20-Aug-2001)
|
|
Ref |
Expression |
|
Hypothesis |
pm2.24i.1 |
|- ph |
|
Assertion |
pm2.24i |
|- ( -. ph -> ps ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pm2.24i.1 |
|- ph |
| 2 |
1
|
a1i |
|- ( -. ps -> ph ) |
| 3 |
2
|
con1i |
|- ( -. ph -> ps ) |