Description: Deduce an equivalence from two implications. Deduction associated with impbi and impbii . (Contributed by NM, 24-Jan-1993) Prove it from impbid21d . (Revised by Wolf Lammen, 3-Nov-2012)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | impbid.1 | |- ( ph -> ( ps -> ch ) ) |
|
| impbid.2 | |- ( ph -> ( ch -> ps ) ) |
||
| Assertion | impbid | |- ( ph -> ( ps <-> ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | impbid.1 | |- ( ph -> ( ps -> ch ) ) |
|
| 2 | impbid.2 | |- ( ph -> ( ch -> ps ) ) |
|
| 3 | 1 2 | impbid21d | |- ( ph -> ( ph -> ( ps <-> ch ) ) ) |
| 4 | 3 | pm2.43i | |- ( ph -> ( ps <-> ch ) ) |