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  7192  xnegpnf  9932  xnegmnf  9933  xaddpnf1  9950  xaddpnf2  9951  xaddmnf1  9952  xaddmnf2  9953  pnfaddmnf  9954  mnfaddpnf  9955  iseqf1olemqk  10633  exp0  10669  sumsnf  11639  prodsnf  11822  lcm0val  12306  ennnfonelemj0  12691  ennnfonelem0  12695  mulg0  13379  lgs0  15408  lgs2  15412  2lgs2  15497  peano3nninf  15808  dceqnconst  15863