Description: The antecedent of one side of a biconditional can be moved out of the biconditional to become the antecedent of the remaining biconditional. (Contributed by BJ, 1-Jan-2025) (Proof shortened by Wolf Lammen, 5-Jan-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | imbibi | |- ( ( ( ph -> ps ) <-> ch ) -> ( ph -> ( ps <-> ch ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.4 | |- ( ( ph -> ( ph -> ps ) ) <-> ( ph -> ps ) ) |
|
2 | imbi2 | |- ( ( ( ph -> ps ) <-> ch ) -> ( ( ph -> ( ph -> ps ) ) <-> ( ph -> ch ) ) ) |
|
3 | 1 2 | bitr3id | |- ( ( ( ph -> ps ) <-> ch ) -> ( ( ph -> ps ) <-> ( ph -> ch ) ) ) |
4 | 3 | pm5.74rd | |- ( ( ( ph -> ps ) <-> ch ) -> ( ph -> ( ps <-> ch ) ) ) |