Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 16-May-1993) (Proof shortened by Wolf Lammen, 25-Oct-2012)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mpbii.min | |- ps |
|
| mpbii.maj | |- ( ph -> ( ps <-> ch ) ) |
||
| Assertion | mpbii | |- ( ph -> ch ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mpbii.min | |- ps |
|
| 2 | mpbii.maj | |- ( ph -> ( ps <-> ch ) ) |
|
| 3 | 1 | a1i | |- ( ph -> ps ) |
| 4 | 3 2 | mpbid | |- ( ph -> ch ) |