Theorem wl-ifp-ncond1

Description: If one case of an if- condition is false, the other automatically follows. (Contributed by Wolf Lammen, 21-Jul-2024)

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

Proof

Step	Hyp	Ref	Expression
1		df-ifp	|- ( if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
2		simpr	|- ( ( ph /\ ps ) -> ps )
3	2	con3i	|- ( -. ps -> -. ( ph /\ ps ) )
4		biorf	|- ( -. ( ph /\ ps ) -> ( ( -. ph /\ ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) ) )
5	3 4	syl	|- ( -. ps -> ( ( -. ph /\ ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) ) )
6	1 5	bitr4id	|- ( -. ps -> ( if- ( ph , ps , ch ) <-> ( -. ph /\ ch ) ) )