Metamath Proof Explorer

Theorem ovif

Description: Move a conditional outside of an operation. (Contributed by Thierry Arnoux, 25-Jan-2017)

		Ref	Expression
	Assertion	ovif	\|- ( if ( ph , A , B ) F C ) = if ( ph , ( A F C ) , ( B F C ) )

Step	Hyp	Ref	Expression
1		oveq1	\|- ( if ( ph , A , B ) = A -> ( if ( ph , A , B ) F C ) = ( A F C ) )
2		oveq1	\|- ( if ( ph , A , B ) = B -> ( if ( ph , A , B ) F C ) = ( B F C ) )
3	1 2	ifsb	\|- ( if ( ph , A , B ) F C ) = if ( ph , ( A F C ) , ( B F C ) )

Step

Hyp

Ref

Expression

 |-  ( if ( ph , A , B ) = A -> ( if ( ph , A , B ) F C ) = ( A F C ) )

 |-  ( if ( ph , A , B ) = B -> ( if ( ph , A , B ) F C ) = ( B F C ) )

1 2

 |-  ( if ( ph , A , B ) F C ) = if ( ph , ( A F C ) , ( B F C ) )