Theorem ifpor

Description: The conditional operator implies the disjunction of its possible outputs. Dual statement of anifp . (Contributed by BJ, 1-Oct-2019)

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

Proof

Step	Hyp	Ref	Expression
1		df-ifp	|- ( if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
2		simpr	|- ( ( ph /\ ps ) -> ps )
3		simpr	|- ( ( -. ph /\ ch ) -> ch )
4	2 3	orim12i	|- ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) -> ( ps \/ ch ) )
5	1 4	sylbi	|- ( if- ( ph , ps , ch ) -> ( ps \/ ch ) )