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 | ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜑 ↔ 𝜒 ) → ( 𝜓 ↔ 𝜒 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | 1 | bicomd | ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( 𝜓 ↔ 𝜑 ) ) |
| 3 | id | ⊢ ( ( 𝜑 ↔ 𝜒 ) → ( 𝜑 ↔ 𝜒 ) ) | |
| 4 | 3 | bicomd | ⊢ ( ( 𝜑 ↔ 𝜒 ) → ( 𝜒 ↔ 𝜑 ) ) |
| 5 | biantr | ⊢ ( ( ( 𝜓 ↔ 𝜑 ) ∧ ( 𝜒 ↔ 𝜑 ) ) → ( 𝜓 ↔ 𝜒 ) ) | |
| 6 | 5 | ex | ⊢ ( ( 𝜓 ↔ 𝜑 ) → ( ( 𝜒 ↔ 𝜑 ) → ( 𝜓 ↔ 𝜒 ) ) ) |
| 7 | 2 4 6 | syl2im | ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜑 ↔ 𝜒 ) → ( 𝜓 ↔ 𝜒 ) ) ) |