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