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  7210  xnegpnf  9950  xnegmnf  9951  xaddpnf1  9968  xaddpnf2  9969  xaddmnf1  9970  xaddmnf2  9971  pnfaddmnf  9972  mnfaddpnf  9973  iseqf1olemqk  10652  exp0  10688  swrd00g  11102  sumsnf  11720  prodsnf  11903  lcm0val  12387  ennnfonelemj0  12772  ennnfonelem0  12776  mulg0  13461  lgs0  15490  lgs2  15494  2lgs2  15579  peano3nninf  15944  dceqnconst  15999