Theorem iftrued 3647

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  ifcif 3638

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-if 3639

This theorem is used by:  ifeq2dadc  3672  eqifdc  3677  ifeqeqxdc  3687  mposnif  6182  fimax2gtrilemstep  7205  2omap  7319  updjudhcoinlf  7421  omp1eomlem  7435  difinfsnlem  7440  ctssdclemn0  7451  ctssdc  7454  enumctlemm  7455  nnnninfeq  7469  nninfisollemne  7472  fodju0  7488  nninfwlpoimlemg  7516  nninfwlpoimlemginf  7517  indconst1  9306  iseqf1olemnab  10952  iseqf1olemab  10953  iseqf1olemqk  10958  iseqf1olemfvp  10961  seq3f1olemqsumkj  10962  seq3f1olemqsum  10964  seq3f1oleml  10967  seq3f1o  10968  fser0const  10986  expnnval  10993  swrdval2  11438  swrdlend  11445  swrd0g  11447  2zsupmax  12008  2zinfmin  12027  xrmaxifle  12030  xrmaxiflemab  12031  xrmaxiflemlub  12032  xrmaxiflemcom  12033  summodclem3  12165  summodclem2a  12166  isum  12170  fsum3  12172  isumss  12176  fsumcl2lem  12183  fsumadd  12191  fsummulc2  12233  cvgratz  12317  prodmodclem3  12360  prodmodclem2a  12361  fprodseq  12368  prod1dc  12371  fprodmul  12376  ef0lem  12445  gcdval  12754  nninfctlemfo  12835  pcmpt  13144  pcmpt2  13145  ballotfilemsgt1  13305  ballotfilemsel1i  13307  ballotfilemsi  13309  ennnfonelemss  13352  ennnfonelemkh  13354  ennnfonelemhf1o  13355  fvprif  13715  gzsumcl  13855  mulgnn  13980  gzsumreidx  14192  gzsumsubmcl  14193  gzsummhm  14196  znf1o  15037  dvply1  15918  lgsdir2  16274  lgsne0  16279  gausslemma2dlem1a  16299  gausslemma2dlem1f1o  16301  gausslemma2dlem2  16303  1loopgrvd2fi  16668  1hevtxdg1en  16671  eupth2lem3lem4fi  16836  bj-charfun  16955  bj-charfundc  16956  subctctexmid  17152  nninfsellemeq  17179  nninfsellemeqinf  17181  nninffeq  17185  dcapnconst  17233