Description: Equivalence deduction for conditional operator for propositions. Convenience theorem for a frequent case. (Contributed by Wolf Lammen, 28-Apr-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ifpbi23d.1 | |
|
ifpbi23d.2 | |
||
Assertion | ifpbi23d | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifpbi23d.1 | |
|
2 | ifpbi23d.2 | |
|
3 | biidd | |
|
4 | 3 1 2 | ifpbi123d | |