Description: Virtual deduction proof of bitr3 353. 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:: | ⊢ ( (𝜑 ↔ 𝜓) ▶ (𝜑
↔ 𝜓) )
| 2:1,?: e1a 42217 | ⊢ ( (𝜑 ↔ 𝜓) ▶ (𝜓
↔ 𝜑) )
| 3:: | ⊢ ( (𝜑 ↔ 𝜓) , (𝜑 ↔ 𝜒)
▶ (𝜑 ↔ 𝜒) )
| 4:3,?: e2 42221 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜑 ↔ 𝜒)
▶ (𝜒 ↔ 𝜑) )
| 5:2,4,?: e12 42314 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜑 ↔ 𝜒)
▶ (𝜓 ↔ 𝜒) )
| 6:5: | ⊢ ( (𝜑 ↔ 𝜓) ▶ ((𝜑
↔ 𝜒) → (𝜓 ↔ 𝜒)) )
| qed:6: | ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒)
→ (𝜓 ↔ 𝜒)))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is
discouraged.) |