Description: A syllogism inference from two biconditionals. This is in the process of being renamed to bitrid (New usages should use bitrid ). (Contributed by NM, 12-Mar-1993)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | syl5bb.1 | |- ( ph <-> ps ) |
|
| syl5bb.2 | |- ( ch -> ( ps <-> th ) ) |
||
| Assertion | syl5bb | |- ( ch -> ( ph <-> th ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | syl5bb.1 | |- ( ph <-> ps ) |
|
| 2 | syl5bb.2 | |- ( ch -> ( ps <-> th ) ) |
|
| 3 | 1 | a1i | |- ( ch -> ( ph <-> ps ) ) |
| 4 | 3 2 | bitrd | |- ( ch -> ( ph <-> th ) ) |