Theorem iftrued 3568

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

Syntax hints:   → wi 4   = wceq 1364  ifcif 3561

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-if 3562

This theorem is referenced by:  ifeq2dadc  3592  eqifdc  3596  mposnif  6016  fimax2gtrilemstep  6961  updjudhcoinlf  7146  omp1eomlem  7160  difinfsnlem  7165  ctssdclemn0  7176  ctssdc  7179  enumctlemm  7180  nnnninfeq  7194  nninfisollemne  7197  fodju0  7213  nninfwlpoimlemg  7241  nninfwlpoimlemginf  7242  iseqf1olemnab  10593  iseqf1olemab  10594  iseqf1olemqk  10599  iseqf1olemfvp  10602  seq3f1olemqsumkj  10603  seq3f1olemqsum  10605  seq3f1oleml  10608  seq3f1o  10609  fser0const  10627  expnnval  10634  2zsupmax  11391  2zinfmin  11408  xrmaxifle  11411  xrmaxiflemab  11412  xrmaxiflemlub  11413  xrmaxiflemcom  11414  summodclem3  11545  summodclem2a  11546  isum  11550  fsum3  11552  isumss  11556  fsumcl2lem  11563  fsumadd  11571  fsummulc2  11613  cvgratz  11697  prodmodclem3  11740  prodmodclem2a  11741  fprodseq  11748  prod1dc  11751  fprodmul  11756  ef0lem  11825  gcdval  12126  nninfctlemfo  12207  pcmpt  12512  pcmpt2  12513  ennnfonelemss  12627  ennnfonelemkh  12629  ennnfonelemhf1o  12630  fvprif  12986  gsumfzz  13127  gsumfzcl  13131  mulgnn  13256  gsumfzreidx  13467  gsumfzsubmcl  13468  gsumfzmptfidmadd  13469  gsumfzmhm  13473  znf1o  14207  dvply1  15001  lgsdir2  15274  lgsne0  15279  gausslemma2dlem1a  15299  gausslemma2dlem1f1o  15301  gausslemma2dlem2  15303  bj-charfun  15453  bj-charfundc  15454  subctctexmid  15645  nninfsellemeq  15658  nninfsellemeqinf  15660  nninffeq  15664  dcapnconst  15705