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  6185  fimax2gtrilemstep  7210  2omap  7325  updjudhcoinlf  7427  omp1eomlem  7441  difinfsnlem  7446  ctssdclemn0  7457  ctssdc  7460  enumctlemm  7461  nnnninfeq  7475  nninfisollemne  7478  fodju0  7494  nninfwlpoimlemg  7522  nninfwlpoimlemginf  7523  indconst1  9313  iseqf1olemnab  10960  iseqf1olemab  10961  iseqf1olemqk  10966  iseqf1olemfvp  10969  seq3f1olemqsumkj  10970  seq3f1olemqsum  10972  seq3f1oleml  10975  seq3f1o  10976  fser0const  10994  expnnval  11001  swrdval2  11446  swrdlend  11453  swrd0g  11455  2zsupmax  12016  2zinfmin  12035  xrmaxifle  12038  xrmaxiflemab  12039  xrmaxiflemlub  12040  xrmaxiflemcom  12041  summodclem3  12173  summodclem2a  12174  isum  12178  fsum3  12180  isumss  12184  fsumcl2lem  12191  fsumadd  12199  fsummulc2  12241  cvgratz  12325  prodmodclem3  12368  prodmodclem2a  12369  fprodseq  12376  prod1dc  12379  fprodmul  12384  ef0lem  12453  gcdval  12762  nninfctlemfo  12843  pcmpt  13152  pcmpt2  13153  ballotfilemsgt1  13313  ballotfilemsel1i  13315  ballotfilemsi  13317  ennnfonelemss  13360  ennnfonelemkh  13362  ennnfonelemhf1o  13363  fvprif  13724  gzsumcl  13864  mulgnn  13989  gzsumreidx  14232  gzsumsubmcl  14233  gzsummhm  14236  znf1o  15096  dvply1  16003  lgsdir2  16369  lgsne0  16374  gausslemma2dlem1a  16394  gausslemma2dlem1f1o  16396  gausslemma2dlem2  16398  1loopgrvd2fi  16763  1hevtxdg1en  16766  eupth2lem3lem4fi  16931  bj-charfun  17050  bj-charfundc  17051  subctctexmid  17247  idjudju  17264  nninfsellemeq  17275  nninfsellemeqinf  17277  nninffeq  17281  dcapnconst  17330