Description: Implication of conditional logical operators. (Contributed by RP, 18-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | ifpim1g | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifpim123g | |
|
2 | id | |
|
3 | 2 | olci | |
4 | 3 | biantrur | |
5 | 4 | bicomi | |
6 | id | |
|
7 | 6 | olci | |
8 | 7 | biantru | |
9 | 8 | bicomi | |
10 | 5 9 | anbi12i | |
11 | 1 10 | bitri | |