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 ( ph , F , G ) B ) = if ( ph , ( A F B ) , ( A G B ) )

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

Step

Hyp

Ref

Expression

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

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

1 2

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