Description: Conjoin both sides of two equivalences. (Contributed by NM, 12-Mar-1993)
Ref | Expression | ||
---|---|---|---|
Hypotheses | anbi12.1 | |- ( ph <-> ps ) |
|
anbi12.2 | |- ( ch <-> th ) |
||
Assertion | anbi12i | |- ( ( ph /\ ch ) <-> ( ps /\ th ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anbi12.1 | |- ( ph <-> ps ) |
|
2 | anbi12.2 | |- ( ch <-> th ) |
|
3 | 2 | anbi2i | |- ( ( ph /\ ch ) <-> ( ph /\ th ) ) |
4 | 3 1 | bianbi | |- ( ( ph /\ ch ) <-> ( ps /\ th ) ) |