Theorem iftrued 3628

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

Syntax hints:   → wi 4   = wceq 1398  ifcif 3619

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 3620

This theorem is referenced by:  ifeq2dadc  3653  eqifdc  3658  mposnif  6146  fimax2gtrilemstep  7157  2omap  7268  updjudhcoinlf  7370  omp1eomlem  7384  difinfsnlem  7389  ctssdclemn0  7400  ctssdc  7403  enumctlemm  7404  nnnninfeq  7418  nninfisollemne  7421  fodju0  7437  nninfwlpoimlemg  7465  nninfwlpoimlemginf  7466  iseqf1olemnab  10862  iseqf1olemab  10863  iseqf1olemqk  10868  iseqf1olemfvp  10871  seq3f1olemqsumkj  10872  seq3f1olemqsum  10874  seq3f1oleml  10877  seq3f1o  10878  fser0const  10896  expnnval  10903  swrdval2  11339  swrdlend  11346  swrd0g  11348  2zsupmax  11907  2zinfmin  11924  xrmaxifle  11927  xrmaxiflemab  11928  xrmaxiflemlub  11929  xrmaxiflemcom  11930  summodclem3  12062  summodclem2a  12063  isum  12067  fsum3  12069  isumss  12073  fsumcl2lem  12080  fsumadd  12088  fsummulc2  12130  cvgratz  12214  prodmodclem3  12257  prodmodclem2a  12258  fprodseq  12265  prod1dc  12268  fprodmul  12273  ef0lem  12342  gcdval  12651  nninfctlemfo  12732  pcmpt  13037  pcmpt2  13038  ennnfonelemss  13153  ennnfonelemkh  13155  ennnfonelemhf1o  13156  fvprif  13548  gsumfzz  13700  gsumfzcl  13704  mulgnn  13835  gsumfzreidx  14046  gsumfzsubmcl  14047  gsumfzmptfidmadd  14048  gsumfzmhm  14052  znf1o  14791  dvply1  15622  lgsdir2  15898  lgsne0  15903  gausslemma2dlem1a  15923  gausslemma2dlem1f1o  15925  gausslemma2dlem2  15927  1loopgrvd2fi  16292  1hevtxdg1en  16295  eupth2lem3lem4fi  16460  bj-charfun  16569  bj-charfundc  16570  subctctexmid  16766  nninfsellemeq  16784  nninfsellemeqinf  16786  nninffeq  16790  dcapnconst  16838