Description: Reverse distribution of implication over biconditional (deduction form). (Contributed by Zhi Wang, 6-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | pm5.32dra.1 | ⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜃 ) ) ) | |
Assertion | pm5.32dra | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 ↔ 𝜃 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.32dra.1 | ⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜃 ) ) ) | |
2 | pm5.32 | ⊢ ( ( 𝜓 → ( 𝜒 ↔ 𝜃 ) ) ↔ ( ( 𝜓 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜃 ) ) ) | |
3 | 1 2 | sylibr | ⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 ↔ 𝜃 ) ) ) |
4 | 3 | imp | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 ↔ 𝜃 ) ) |