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φBCφA=B¬φA=C

Proof

Step Hyp Ref Expression
1 eqeq2 ifφBC=BA=ifφBCA=B
2 eqeq2 ifφBC=CA=ifφBCA=C
3 1 2 elimif A=ifφBCφA=B¬φA=C