Metamath Proof Explorer


Theorem ifov

Description: Move a conditional outside of an operation. (Contributed by AV, 11-Nov-2019)

Ref Expression
Assertion ifov A if φ F G B = if φ A F B A G B

Proof

Step Hyp Ref Expression
1 oveq if φ F G = F A if φ F G B = A F B
2 oveq if φ F G = G A if φ F G B = A G B
3 1 2 ifsb A if φ F G B = if φ A F B A G B