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

Metamath Proof Explorer

Theorem iffv

Description: Move a conditional outside of a function. (Contributed by Thierry Arnoux, 28-Sep-2018)

Ref Expression
Assertion iffv ⊢ if φ F G ⁡ A = if φ F ⁡ A G ⁡ A

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ if φ F G = F → if φ F G ⁡ A = F ⁡ A
2 fveq1 ⊢ if φ F G = G → if φ F G ⁡ A = G ⁡ A
3 1 2 ifsb ⊢ if φ F G ⁡ A = if φ F ⁡ A G ⁡ A