Theorem iftruei 3585

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

Hypothesis

Ref	Expression
iftruei.1	|- ph

Assertion

Ref	Expression
iftruei	|- if ( ph , A , B ) = A

Proof of Theorem iftruei

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

Syntax hints:   = wceq 1373   ifcif 3579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-if 3580

This theorem is referenced by:  ctmlemr  7236  xnegpnf  9985  xnegmnf  9986  xaddpnf1  10003  xaddpnf2  10004  xaddmnf1  10005  xaddmnf2  10006  pnfaddmnf  10007  mnfaddpnf  10008  iseqf1olemqk  10689  exp0  10725  swrd00g  11140  sumsnf  11835  prodsnf  12018  lcm0val  12502  ennnfonelemj0  12887  ennnfonelem0  12891  mulg0  13576  lgs0  15605  lgs2  15609  2lgs2  15694  peano3nninf  16146  dceqnconst  16201