Theorem iftruei

Description: Inference associated with iftrue . (Contributed by BJ, 7-Oct-2018)

	Ref	Expression
Hypothesis	iftruei.1	|- ph
Assertion	iftruei	|- if ( ph , A , B ) = A

Proof

Step	Hyp	Ref	Expression
1		iftruei.1	|- ph
2		iftrue	|- ( ph -> if ( ph , A , B ) = A )
3	1 2	ax-mp	|- if ( ph , A , B ) = A