Theorem dfifp6

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

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

Proof

Step	Hyp	Ref	Expression
1		df-ifp	|- ( if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
2		ancom	|- ( ( -. ph /\ ch ) <-> ( ch /\ -. ph ) )
3		annim	|- ( ( ch /\ -. ph ) <-> -. ( ch -> ph ) )
4	2 3	bitri	|- ( ( -. ph /\ ch ) <-> -. ( ch -> ph ) )
5	4	orbi2i	|- ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) <-> ( ( ph /\ ps ) \/ -. ( ch -> ph ) ) )
6	1 5	bitri	|- ( if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ -. ( ch -> ph ) ) )