Theorem dfifp7

Description: Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019)

	Ref	Expression
Assertion	dfifp7	|- ( if- ( ph , ps , ch ) <-> ( ( ch -> ph ) -> ( ph /\ ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		orcom	|- ( ( ( ph /\ ps ) \/ -. ( ch -> ph ) ) <-> ( -. ( ch -> ph ) \/ ( ph /\ ps ) ) )
2		dfifp6	|- ( if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ -. ( ch -> ph ) ) )
3		imor	|- ( ( ( ch -> ph ) -> ( ph /\ ps ) ) <-> ( -. ( ch -> ph ) \/ ( ph /\ ps ) ) )
4	1 2 3	3bitr4i	|- ( if- ( ph , ps , ch ) <-> ( ( ch -> ph ) -> ( ph /\ ps ) ) )