Description: Adding biconditional when antecedents are conjuncted. (Contributed by metakunt, 16-Apr-2024) (Proof shortened by Wolf Lammen, 7-May-2025) (Proof shortened by Garrett Katz, 15-Jun-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | anbiim.1 | |- ( ph -> ( ch -> th ) ) |
|
| anbiim.2 | |- ( ps -> ( th -> ch ) ) |
||
| Assertion | anbiim | |- ( ( ph /\ ps ) -> ( ch <-> th ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | anbiim.1 | |- ( ph -> ( ch -> th ) ) |
|
| 2 | anbiim.2 | |- ( ps -> ( th -> ch ) ) |
|
| 3 | 1 2 | impbid21d | |- ( ps -> ( ph -> ( ch <-> th ) ) ) |
| 4 | 3 | impcom | |- ( ( ph /\ ps ) -> ( ch <-> th ) ) |