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  7211  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  10959  iseqf1olemab  10960  iseqf1olemqk  10965  iseqf1olemfvp  10968  seq3f1olemqsumkj  10969  seq3f1olemqsum  10971  seq3f1oleml  10974  seq3f1o  10975  fser0const  10993  expnnval  11000  swrdval2  11445  swrdlend  11452  swrd0g  11454  2zsupmax  12015  2zinfmin  12034  xrmaxifle  12037  xrmaxiflemab  12038  xrmaxiflemlub  12039  xrmaxiflemcom  12040  summodclem3  12172  summodclem2a  12173  isum  12177  fsum3  12179  isumss  12183  fsumcl2lem  12190  fsumadd  12198  fsummulc2  12240  cvgratz  12324  prodmodclem3  12367  prodmodclem2a  12368  fprodseq  12375  prod1dc  12378  fprodmul  12383  ef0lem  12452  gcdval  12761  nninfctlemfo  12842  pcmpt  13151  pcmpt2  13152  ballotfilemsgt1  13312  ballotfilemsel1i  13314  ballotfilemsi  13316  ennnfonelemss  13359  ennnfonelemkh  13361  ennnfonelemhf1o  13362  fvprif  13723  gzsumcl  13863  mulgnn  13988  gzsumreidx  14231  gzsumsubmcl  14232  gzsummhm  14235  znf1o  15095  dvply1  16024  lgsdir2  16390  lgsne0  16395  gausslemma2dlem1a  16415  gausslemma2dlem1f1o  16417  gausslemma2dlem2  16419  1loopgrvd2fi  16784  1hevtxdg1en  16787  eupth2lem3lem4fi  16952  bj-charfun  17071  bj-charfundc  17072  subctctexmid  17268  idjudju  17285  nninfsellemeq  17296  nninfsellemeqinf  17298  nninffeq  17302  dcapnconst  17351