Description: Given the hypotheses there exists a proof for (c implies ( d iff a ) ). (Contributed by Jarvin Udandy, 6-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | confun.1 | |
|
confun.2 | |
||
confun.3 | |
||
confun.4 | |
||
Assertion | confun | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | confun.1 | |
|
2 | confun.2 | |
|
3 | confun.3 | |
|
4 | confun.4 | |
|
5 | ax-1 | |
|
6 | 3 | a1i | |
7 | 5 6 | impbid | |
8 | 1 4 | ax-mp | |
9 | ax-1 | |
|
10 | 1 9 | ax-mp | |
11 | 8 10 | impbii | |
12 | 2 11 | sylibr | |
13 | 12 | a1i | |
14 | ax-1 | |
|
15 | 13 14 | impbid | |
16 | 7 15 | bitrd | |