Theorem iftrued 3400

Description: Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypothesis

Ref	Expression
iftrued.1	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
iftrued	⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)

Proof of Theorem iftrued

Step	Hyp	Ref	Expression
1		iftrued.1	. 2 ⊢ (𝜑 → 𝜒)
2		iftrue 3398	. 2 ⊢ (𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1289  ifcif 3393

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-if 3394

This theorem is referenced by:  eqifdc  3425  fimax2gtrilemstep  6614  updjudhcoinlf  6769  fodjuomnilem0  6800  iseqf1olemnab  9913  iseqf1olemab  9914  iseqf1olemqk  9919  iseqf1olemfvp  9922  seq3f1olemqsumkj  9923  seq3f1olemqsum  9925  seq3f1oleml  9928  seq3f1o  9929  fser0const  9947  expnnval  9954  2zsupmax  10653  isummolem3  10766  isummolem2a  10767  iisum  10771  fisum  10774  isumss  10779  fsumcl2lem  10788  fsumadd  10796  fsummulc2  10838  cvgratz  10922  ef0lem  10946  gcdval  11225  ressid2  11546  nninfalllemn  11853  nninfsellemeq  11861  nninfsellemeqinf  11863