Metamath Proof Explorer

Theorem ovif2

Description: Move a conditional outside of an operation. (Contributed by Thierry Arnoux, 1-Oct-2018)

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

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

Step

Hyp

Ref

Expression

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

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

1 2

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