Theorem iftruei 3577

Description: Inference associated with iftrue 3576. (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 3576	. 2 |- ( ph -> if ( ph , A , B ) = A )
3	1, 2	ax-mp 5	1 |- if ( ph , A , B ) = A

Syntax hints:   = wceq 1373   ifcif 3571

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-if 3572

This theorem is referenced by:  ctmlemr  7212  xnegpnf  9952  xnegmnf  9953  xaddpnf1  9970  xaddpnf2  9971  xaddmnf1  9972  xaddmnf2  9973  pnfaddmnf  9974  mnfaddpnf  9975  iseqf1olemqk  10654  exp0  10690  swrd00g  11105  sumsnf  11753  prodsnf  11936  lcm0val  12420  ennnfonelemj0  12805  ennnfonelem0  12809  mulg0  13494  lgs0  15523  lgs2  15527  2lgs2  15612  peano3nninf  15981  dceqnconst  16036