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  7318  updjudhcoinlf  7420  omp1eomlem  7434  difinfsnlem  7439  ctssdclemn0  7450  ctssdc  7453  enumctlemm  7454  nnnninfeq  7468  nninfisollemne  7471  fodju0  7487  nninfwlpoimlemg  7515  nninfwlpoimlemginf  7516  indconst1  9304  iseqf1olemnab  10940  iseqf1olemab  10941  iseqf1olemqk  10946  iseqf1olemfvp  10949  seq3f1olemqsumkj  10950  seq3f1olemqsum  10952  seq3f1oleml  10955  seq3f1o  10956  fser0const  10974  expnnval  10981  swrdval2  11425  swrdlend  11432  swrd0g  11434  2zsupmax  11994  2zinfmin  12011  xrmaxifle  12014  xrmaxiflemab  12015  xrmaxiflemlub  12016  xrmaxiflemcom  12017  summodclem3  12149  summodclem2a  12150  isum  12154  fsum3  12156  isumss  12160  fsumcl2lem  12167  fsumadd  12175  fsummulc2  12217  cvgratz  12301  prodmodclem3  12344  prodmodclem2a  12345  fprodseq  12352  prod1dc  12355  fprodmul  12360  ef0lem  12429  gcdval  12738  nninfctlemfo  12819  pcmpt  13124  pcmpt2  13125  ballotfilemsgt1  13256  ballotfilemsel1i  13258  ballotfilemsi  13260  ennnfonelemss  13303  ennnfonelemkh  13305  ennnfonelemhf1o  13306  fvprif  13666  gzsumcl  13806  mulgnn  13931  gzsumreidx  14143  gzsumsubmcl  14144  gzsummhm  14147  znf1o  14988  dvply1  15868  lgsdir2  16164  lgsne0  16169  gausslemma2dlem1a  16189  gausslemma2dlem1f1o  16191  gausslemma2dlem2  16193  1loopgrvd2fi  16558  1hevtxdg1en  16561  eupth2lem3lem4fi  16726  bj-charfun  16845  bj-charfundc  16846  subctctexmid  17042  nninfsellemeq  17069  nninfsellemeqinf  17071  nninffeq  17075  dcapnconst  17123