Theorem iftrued 3629

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

Syntax hints:   → wi 4   = wceq 1398  ifcif 3620

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 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-if 3621

This theorem is referenced by:  ifeq2dadc  3654  eqifdc  3659  mposnif  6147  fimax2gtrilemstep  7158  2omap  7269  updjudhcoinlf  7371  omp1eomlem  7385  difinfsnlem  7390  ctssdclemn0  7401  ctssdc  7404  enumctlemm  7405  nnnninfeq  7419  nninfisollemne  7422  fodju0  7438  nninfwlpoimlemg  7466  nninfwlpoimlemginf  7467  iseqf1olemnab  10863  iseqf1olemab  10864  iseqf1olemqk  10869  iseqf1olemfvp  10872  seq3f1olemqsumkj  10873  seq3f1olemqsum  10875  seq3f1oleml  10878  seq3f1o  10879  fser0const  10897  expnnval  10904  swrdval2  11341  swrdlend  11348  swrd0g  11350  2zsupmax  11909  2zinfmin  11926  xrmaxifle  11929  xrmaxiflemab  11930  xrmaxiflemlub  11931  xrmaxiflemcom  11932  summodclem3  12064  summodclem2a  12065  isum  12069  fsum3  12071  isumss  12075  fsumcl2lem  12082  fsumadd  12090  fsummulc2  12132  cvgratz  12216  prodmodclem3  12259  prodmodclem2a  12260  fprodseq  12267  prod1dc  12270  fprodmul  12275  ef0lem  12344  gcdval  12653  nninfctlemfo  12734  pcmpt  13039  pcmpt2  13040  ennnfonelemss  13159  ennnfonelemkh  13161  ennnfonelemhf1o  13162  fvprif  13554  gsumfzz  13706  gsumfzcl  13710  mulgnn  13841  gsumfzreidx  14052  gsumfzsubmcl  14053  gsumfzmptfidmadd  14054  gsumfzmhm  14058  znf1o  14797  dvply1  15628  lgsdir2  15904  lgsne0  15909  gausslemma2dlem1a  15929  gausslemma2dlem1f1o  15931  gausslemma2dlem2  15933  1loopgrvd2fi  16298  1hevtxdg1en  16301  eupth2lem3lem4fi  16466  bj-charfun  16575  bj-charfundc  16576  subctctexmid  16772  nninfsellemeq  16790  nninfsellemeqinf  16792  nninffeq  16796  dcapnconst  16845