Metamath Proof Explorer

Theorem eqif

Description: Expansion of an equality with a conditional operator. (Contributed by NM, 14-Feb-2005)

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

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

Step

Hyp

Ref

Expression

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

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

1 2

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