Theorem iftruei 3552

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

Syntax hints:   = wceq 1363   ifcif 3546

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 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-if 3547

This theorem is referenced by:  ctmlemr  7121  xnegpnf  9842  xnegmnf  9843  xaddpnf1  9860  xaddpnf2  9861  xaddmnf1  9862  xaddmnf2  9863  pnfaddmnf  9864  mnfaddpnf  9865  iseqf1olemqk  10508  exp0  10538  sumsnf  11431  prodsnf  11614  lcm0val  12079  ennnfonelemj0  12416  ennnfonelem0  12420  mulg0  13020  lgs0  14710  lgs2  14714  peano3nninf  15053  dceqnconst  15105