Description: Reverse distribution of implication over biconditional (deduction form). (Contributed by Zhi Wang, 6-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | pm5.32dra.1 | |- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) ) |
|
Assertion | pm5.32dra | |- ( ( ph /\ ps ) -> ( ch <-> th ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.32dra.1 | |- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) ) |
|
2 | pm5.32 | |- ( ( ps -> ( ch <-> th ) ) <-> ( ( ps /\ ch ) <-> ( ps /\ th ) ) ) |
|
3 | 1 2 | sylibr | |- ( ph -> ( ps -> ( ch <-> th ) ) ) |
4 | 3 | imp | |- ( ( ph /\ ps ) -> ( ch <-> th ) ) |