Description: Obsolete version of anbiim as of 15-Jun-2026. Adding biconditional when antecedents are conjuncted. (Contributed by metakunt, 16-Apr-2024) (Proof shortened by Wolf Lammen, 7-May-2025) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | anbiim.1 | |- ( ph -> ( ch -> th ) ) |
|
| anbiim.2 | |- ( ps -> ( th -> ch ) ) |
||
| Assertion | anbiimOLD | |- ( ( ph /\ ps ) -> ( ch <-> th ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | anbiim.1 | |- ( ph -> ( ch -> th ) ) |
|
| 2 | anbiim.2 | |- ( ps -> ( th -> ch ) ) |
|
| 3 | 1 | adantr | |- ( ( ph /\ ps ) -> ( ch -> th ) ) |
| 4 | 2 | adantl | |- ( ( ph /\ ps ) -> ( th -> ch ) ) |
| 5 | 3 4 | impbid | |- ( ( ph /\ ps ) -> ( ch <-> th ) ) |