Description: Separation of the values of the conditional operator for propositions. (Contributed by AV, 30-Dec-2020) (Proof shortened by Wolf Lammen, 27-Feb-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ifpimpda.1 | |
|
ifpimpda.2 | |
||
Assertion | ifpimpda | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifpimpda.1 | |
|
2 | ifpimpda.2 | |
|
3 | 1 | ex | |
4 | 2 | ex | |
5 | dfifp2 | |
|
6 | 3 4 5 | sylanbrc | |