This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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