Description: Virtual deduction proof of bitr3 . The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
| 1:: | |- (. ( ph <-> ps ) ->. ( ph <-> ps ) ). |
| 2:1,?: e1a | |- (. ( ph <-> ps ) ->. ( ps <-> ph ) ). |
| 3:: | |- (. ( ph <-> ps ) ,. ( ph <-> ch ) ->. ( ph <-> ch ) ). |
| 4:3,?: e2 | |- (. ( ph <-> ps ) ,. ( ph <-> ch ) ->. ( ch <-> ph ) ). |
| 5:2,4,?: e12 | |- (. ( ph <-> ps ) ,. ( ph <-> ch ) ->. ( ps <-> ch ) ). |
| 6:5: | |- (. ( ph <-> ps ) ->. ( ( ph <-> ch ) -> ( ps <-> ch ) ) ). |
| qed:6: | |- ( ( ph <-> ps ) -> ( ( ph <-> ch ) -> ( ps <-> ch ) ) ) |
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bitr3VD | |- ( ( ph <-> ps ) -> ( ( ph <-> ch ) -> ( ps <-> ch ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | |- ( ( ph <-> ps ) -> ( ph <-> ps ) ) |
|
| 2 | 1 | bicomd | |- ( ( ph <-> ps ) -> ( ps <-> ph ) ) |
| 3 | id | |- ( ( ph <-> ch ) -> ( ph <-> ch ) ) |
|
| 4 | 3 | bicomd | |- ( ( ph <-> ch ) -> ( ch <-> ph ) ) |
| 5 | biantr | |- ( ( ( ps <-> ph ) /\ ( ch <-> ph ) ) -> ( ps <-> ch ) ) |
|
| 6 | 5 | ex | |- ( ( ps <-> ph ) -> ( ( ch <-> ph ) -> ( ps <-> ch ) ) ) |
| 7 | 2 4 6 | syl2im | |- ( ( ph <-> ps ) -> ( ( ph <-> ch ) -> ( ps <-> ch ) ) ) |