Theorem iftrued 3539

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 3537	. 2 ⊢ (𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1353  ifcif 3532

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 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-if 3533

This theorem is referenced by:  eqifdc  3566  mposnif  5959  fimax2gtrilemstep  6890  updjudhcoinlf  7069  omp1eomlem  7083  difinfsnlem  7088  ctssdclemn0  7099  ctssdc  7102  enumctlemm  7103  nnnninfeq  7116  nninfisollemne  7119  fodju0  7135  nninfwlpoimlemg  7163  nninfwlpoimlemginf  7164  iseqf1olemnab  10458  iseqf1olemab  10459  iseqf1olemqk  10464  iseqf1olemfvp  10467  seq3f1olemqsumkj  10468  seq3f1olemqsum  10470  seq3f1oleml  10473  seq3f1o  10474  fser0const  10486  expnnval  10493  2zsupmax  11202  2zinfmin  11219  xrmaxifle  11222  xrmaxiflemab  11223  xrmaxiflemlub  11224  xrmaxiflemcom  11225  summodclem3  11356  summodclem2a  11357  isum  11361  fsum3  11363  isumss  11367  fsumcl2lem  11374  fsumadd  11382  fsummulc2  11424  cvgratz  11508  prodmodclem3  11551  prodmodclem2a  11552  fprodseq  11559  prod1dc  11562  fprodmul  11567  ef0lem  11636  gcdval  11927  pcmpt  12308  pcmpt2  12309  ennnfonelemss  12378  ennnfonelemkh  12380  ennnfonelemhf1o  12381  mulgnn  12859  lgsdir2  14014  lgsne0  14019  bj-charfun  14128  bj-charfundc  14129  subctctexmid  14320  nninfsellemeq  14333  nninfsellemeqinf  14335  nninffeq  14339  dcapnconst  14378