Theorem iftruei 3609

Description: Inference associated with iftrue 3608. (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 3608	. 2 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ if(𝜑, 𝐴, 𝐵) = 𝐴

Syntax hints:   = wceq 1395  ifcif 3603

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 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-if 3604

This theorem is referenced by:  ctmlemr  7298  xnegpnf  10053  xnegmnf  10054  xaddpnf1  10071  xaddpnf2  10072  xaddmnf1  10073  xaddmnf2  10074  pnfaddmnf  10075  mnfaddpnf  10076  iseqf1olemqk  10759  exp0  10795  swrd00g  11220  sumsnf  11960  prodsnf  12143  lcm0val  12627  ennnfonelemj0  13012  ennnfonelem0  13016  mulg0  13702  lgs0  15732  lgs2  15736  2lgs2  15821  1loopgrvd2fi  16111  peano3nninf  16545  dceqnconst  16600