Theorem iftrued 3610

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

Syntax hints:   → wi 4   = wceq 1395  ifcif 3603

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 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-if 3604

This theorem is referenced by:  ifeq2dadc  3635  eqifdc  3640  mposnif  6110  fimax2gtrilemstep  7085  updjudhcoinlf  7273  omp1eomlem  7287  difinfsnlem  7292  ctssdclemn0  7303  ctssdc  7306  enumctlemm  7307  nnnninfeq  7321  nninfisollemne  7324  fodju0  7340  nninfwlpoimlemg  7368  nninfwlpoimlemginf  7369  iseqf1olemnab  10756  iseqf1olemab  10757  iseqf1olemqk  10762  iseqf1olemfvp  10765  seq3f1olemqsumkj  10766  seq3f1olemqsum  10768  seq3f1oleml  10771  seq3f1o  10772  fser0const  10790  expnnval  10797  swrdval2  11225  swrdlend  11232  swrd0g  11234  2zsupmax  11780  2zinfmin  11797  xrmaxifle  11800  xrmaxiflemab  11801  xrmaxiflemlub  11802  xrmaxiflemcom  11803  summodclem3  11934  summodclem2a  11935  isum  11939  fsum3  11941  isumss  11945  fsumcl2lem  11952  fsumadd  11960  fsummulc2  12002  cvgratz  12086  prodmodclem3  12129  prodmodclem2a  12130  fprodseq  12137  prod1dc  12140  fprodmul  12145  ef0lem  12214  gcdval  12523  nninfctlemfo  12604  pcmpt  12909  pcmpt2  12910  ennnfonelemss  13024  ennnfonelemkh  13026  ennnfonelemhf1o  13027  fvprif  13419  gsumfzz  13571  gsumfzcl  13575  mulgnn  13706  gsumfzreidx  13917  gsumfzsubmcl  13918  gsumfzmptfidmadd  13919  gsumfzmhm  13923  znf1o  14658  dvply1  15482  lgsdir2  15755  lgsne0  15760  gausslemma2dlem1a  15780  gausslemma2dlem1f1o  15782  gausslemma2dlem2  15784  1loopgrvd2fi  16116  1hevtxdg1en  16119  bj-charfun  16352  bj-charfundc  16353  2omap  16544  subctctexmid  16551  nninfsellemeq  16566  nninfsellemeqinf  16568  nninffeq  16572  dcapnconst  16615