Theorem iftrued 3580

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

Syntax hints:   → wi 4   = wceq 1373  ifcif 3573

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 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-if 3574

This theorem is referenced by:  ifeq2dadc  3604  eqifdc  3609  mposnif  6049  fimax2gtrilemstep  7009  updjudhcoinlf  7194  omp1eomlem  7208  difinfsnlem  7213  ctssdclemn0  7224  ctssdc  7227  enumctlemm  7228  nnnninfeq  7242  nninfisollemne  7245  fodju0  7261  nninfwlpoimlemg  7289  nninfwlpoimlemginf  7290  iseqf1olemnab  10659  iseqf1olemab  10660  iseqf1olemqk  10665  iseqf1olemfvp  10668  seq3f1olemqsumkj  10669  seq3f1olemqsum  10671  seq3f1oleml  10674  seq3f1o  10675  fser0const  10693  expnnval  10700  swrdval2  11118  swrdlend  11125  swrd0g  11127  2zsupmax  11587  2zinfmin  11604  xrmaxifle  11607  xrmaxiflemab  11608  xrmaxiflemlub  11609  xrmaxiflemcom  11610  summodclem3  11741  summodclem2a  11742  isum  11746  fsum3  11748  isumss  11752  fsumcl2lem  11759  fsumadd  11767  fsummulc2  11809  cvgratz  11893  prodmodclem3  11936  prodmodclem2a  11937  fprodseq  11944  prod1dc  11947  fprodmul  11952  ef0lem  12021  gcdval  12330  nninfctlemfo  12411  pcmpt  12716  pcmpt2  12717  ennnfonelemss  12831  ennnfonelemkh  12833  ennnfonelemhf1o  12834  fvprif  13225  gsumfzz  13377  gsumfzcl  13381  mulgnn  13512  gsumfzreidx  13723  gsumfzsubmcl  13724  gsumfzmptfidmadd  13725  gsumfzmhm  13729  znf1o  14463  dvply1  15287  lgsdir2  15560  lgsne0  15565  gausslemma2dlem1a  15585  gausslemma2dlem1f1o  15587  gausslemma2dlem2  15589  bj-charfun  15857  bj-charfundc  15858  2omap  16047  subctctexmid  16052  nninfsellemeq  16066  nninfsellemeqinf  16068  nninffeq  16072  dcapnconst  16115