This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: A mixed syllogism inference from a biconditional and an implication.
(Contributed by Wolf Lammen, 16-Dec-2013)
|
|
Ref |
Expression |
|
Hypotheses |
sylnbir.1 |
|- ( ps <-> ph ) |
|
|
sylnbir.2 |
|- ( -. ps -> ch ) |
|
Assertion |
sylnbir |
|- ( -. ph -> ch ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
sylnbir.1 |
|- ( ps <-> ph ) |
| 2 |
|
sylnbir.2 |
|- ( -. ps -> ch ) |
| 3 |
1
|
bicomi |
|- ( ph <-> ps ) |
| 4 |
3 2
|
sylnbi |
|- ( -. ph -> ch ) |