Description: Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | ifpbi123 | |- ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> ( if- ( ph , ch , ta ) <-> if- ( ps , th , et ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 | |- ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> ( ph <-> ps ) ) |
|
2 | simp2 | |- ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> ( ch <-> th ) ) |
|
3 | simp3 | |- ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> ( ta <-> et ) ) |
|
4 | 1 2 3 | ifpbi123d | |- ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> ( if- ( ph , ch , ta ) <-> if- ( ps , th , et ) ) ) |