Metamath Proof Explorer


Theorem fvifeq

Description: Equality of function values with conditional arguments, see also fvif . (Contributed by Alexander van der Vekens, 21-May-2018)

Ref Expression
Assertion fvifeq A = if φ B C F A = if φ F B F C

Proof

Step Hyp Ref Expression
1 fveq2 A = if φ B C F A = F if φ B C
2 fvif F if φ B C = if φ F B F C
3 1 2 syl6eq A = if φ B C F A = if φ F B F C