Metamath Proof Explorer

Theorem ifval

Description: Another expression of the value of the if predicate, analogous to eqif . See also the more specialized iftrue and iffalse . (Contributed by BJ, 6-Apr-2019)

		Ref	Expression
	Assertion	ifval	\|- ( A = if ( ph , B , C ) <-> ( ( ph -> A = B ) /\ ( -. ph -> A = C ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqif	\|- ( A = if ( ph , B , C ) <-> ( ( ph /\ A = B ) \/ ( -. ph /\ A = C ) ) )
2		cases2	\|- ( ( ( ph /\ A = B ) \/ ( -. ph /\ A = C ) ) <-> ( ( ph -> A = B ) /\ ( -. ph -> A = C ) ) )
3	1 2	bitri	\|- ( A = if ( ph , B , C ) <-> ( ( ph -> A = B ) /\ ( -. ph -> A = C ) ) )

Step

Hyp

Ref

Expression

eqif

 |-  ( A = if ( ph , B , C ) <-> ( ( ph /\ A = B ) \/ ( -. ph /\ A = C ) ) )

cases2

 |-  ( ( ( ph /\ A = B ) \/ ( -. ph /\ A = C ) ) <-> ( ( ph -> A = B ) /\ ( -. ph -> A = C ) ) )

1 2

bitri

 |-  ( A = if ( ph , B , C ) <-> ( ( ph -> A = B ) /\ ( -. ph -> A = C ) ) )