Theorem iftrued 3633

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

Syntax hints:   → wi 4   = wceq 1398  ifcif 3624

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 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-if 3625

This theorem is referenced by:  ifeq2dadc  3658  eqifdc  3663  ifeqeqxdc  3673  mposnif  6155  fimax2gtrilemstep  7171  2omap  7282  updjudhcoinlf  7384  omp1eomlem  7398  difinfsnlem  7403  ctssdclemn0  7414  ctssdc  7417  enumctlemm  7418  nnnninfeq  7432  nninfisollemne  7435  fodju0  7451  nninfwlpoimlemg  7479  nninfwlpoimlemginf  7480  iseqf1olemnab  10890  iseqf1olemab  10891  iseqf1olemqk  10896  iseqf1olemfvp  10899  seq3f1olemqsumkj  10900  seq3f1olemqsum  10902  seq3f1oleml  10905  seq3f1o  10906  fser0const  10924  expnnval  10931  swrdval2  11371  swrdlend  11378  swrd0g  11380  2zsupmax  11940  2zinfmin  11957  xrmaxifle  11960  xrmaxiflemab  11961  xrmaxiflemlub  11962  xrmaxiflemcom  11963  summodclem3  12095  summodclem2a  12096  isum  12100  fsum3  12102  isumss  12106  fsumcl2lem  12113  fsumadd  12121  fsummulc2  12163  cvgratz  12247  prodmodclem3  12290  prodmodclem2a  12291  fprodseq  12298  prod1dc  12301  fprodmul  12306  ef0lem  12375  gcdval  12684  nninfctlemfo  12765  pcmpt  13070  pcmpt2  13071  ballotfilemsgt1  13202  ballotfilemsel1i  13204  ballotfilemsi  13206  ennnfonelemss  13249  ennnfonelemkh  13251  ennnfonelemhf1o  13252  fvprif  13611  gsumfzz  13754  gsumfzcl  13758  mulgnn  13883  gsumfzreidx  14094  gsumfzsubmcl  14095  gsumfzmptfidmadd  14096  gsumfzmhm  14100  znf1o  14929  dvply1  15760  lgsdir2  16036  lgsne0  16041  gausslemma2dlem1a  16061  gausslemma2dlem1f1o  16063  gausslemma2dlem2  16065  1loopgrvd2fi  16430  1hevtxdg1en  16433  eupth2lem3lem4fi  16598  bj-charfun  16717  bj-charfundc  16718  subctctexmid  16914  nninfsellemeq  16932  nninfsellemeqinf  16934  nninffeq  16938  dcapnconst  16986