Theorem iftruei 3576

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

Hypothesis

Ref	Expression
iftruei.1	⊢ 𝜑

Assertion

Ref	Expression
iftruei	⊢ if(𝜑, 𝐴, 𝐵) = 𝐴

Proof of Theorem iftruei

Step	Hyp	Ref	Expression
1		iftruei.1	. 2 ⊢ 𝜑
2		iftrue 3575	. 2 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ if(𝜑, 𝐴, 𝐵) = 𝐴

Syntax hints:   = wceq 1372  ifcif 3570

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-if 3571

This theorem is referenced by:  ctmlemr  7209  xnegpnf  9949  xnegmnf  9950  xaddpnf1  9967  xaddpnf2  9968  xaddmnf1  9969  xaddmnf2  9970  pnfaddmnf  9971  mnfaddpnf  9972  iseqf1olemqk  10650  exp0  10686  sumsnf  11662  prodsnf  11845  lcm0val  12329  ennnfonelemj0  12714  ennnfonelem0  12718  mulg0  13403  lgs0  15432  lgs2  15436  2lgs2  15521  peano3nninf  15877  dceqnconst  15932