Metamath Proof Explorer


Theorem confun

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 χθφ

Proof

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 χθφ