Theorem iftrued 3612

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

Syntax hints:   → wi 4   = wceq 1397  ifcif 3605

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-if 3606

This theorem is referenced by:  ifeq2dadc  3637  eqifdc  3642  mposnif  6115  fimax2gtrilemstep  7090  updjudhcoinlf  7279  omp1eomlem  7293  difinfsnlem  7298  ctssdclemn0  7309  ctssdc  7312  enumctlemm  7313  nnnninfeq  7327  nninfisollemne  7330  fodju0  7346  nninfwlpoimlemg  7374  nninfwlpoimlemginf  7375  iseqf1olemnab  10764  iseqf1olemab  10765  iseqf1olemqk  10770  iseqf1olemfvp  10773  seq3f1olemqsumkj  10774  seq3f1olemqsum  10776  seq3f1oleml  10779  seq3f1o  10780  fser0const  10798  expnnval  10805  swrdval2  11236  swrdlend  11243  swrd0g  11245  2zsupmax  11791  2zinfmin  11808  xrmaxifle  11811  xrmaxiflemab  11812  xrmaxiflemlub  11813  xrmaxiflemcom  11814  summodclem3  11946  summodclem2a  11947  isum  11951  fsum3  11953  isumss  11957  fsumcl2lem  11964  fsumadd  11972  fsummulc2  12014  cvgratz  12098  prodmodclem3  12141  prodmodclem2a  12142  fprodseq  12149  prod1dc  12152  fprodmul  12157  ef0lem  12226  gcdval  12535  nninfctlemfo  12616  pcmpt  12921  pcmpt2  12922  ennnfonelemss  13036  ennnfonelemkh  13038  ennnfonelemhf1o  13039  fvprif  13431  gsumfzz  13583  gsumfzcl  13587  mulgnn  13718  gsumfzreidx  13929  gsumfzsubmcl  13930  gsumfzmptfidmadd  13931  gsumfzmhm  13935  znf1o  14671  dvply1  15495  lgsdir2  15768  lgsne0  15773  gausslemma2dlem1a  15793  gausslemma2dlem1f1o  15795  gausslemma2dlem2  15797  1loopgrvd2fi  16162  1hevtxdg1en  16165  eupth2lem3lem4fi  16330  bj-charfun  16428  bj-charfundc  16429  2omap  16620  subctctexmid  16627  nninfsellemeq  16642  nninfsellemeqinf  16644  nninffeq  16648  dcapnconst  16691