Description: A deduction eliminating a conjunct, similar to simplbi2 . (Contributed by Alan Sare, 22-Jul-2012) (Proof shortened by Wolf Lammen, 10-Nov-2012)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | simplbi2com.1 | |- ( ph <-> ( ps /\ ch ) ) |
|
| Assertion | simplbi2com | |- ( ch -> ( ps -> ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simplbi2com.1 | |- ( ph <-> ( ps /\ ch ) ) |
|
| 2 | 1 | simplbi2 | |- ( ps -> ( ch -> ph ) ) |
| 3 | 2 | com12 | |- ( ch -> ( ps -> ph ) ) |