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