Theorem iftrued 3556

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

Syntax hints:   → wi 4   = wceq 1364  ifcif 3549

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-if 3550

This theorem is referenced by:  ifeq2dadc  3580  eqifdc  3584  mposnif  5990  fimax2gtrilemstep  6928  updjudhcoinlf  7109  omp1eomlem  7123  difinfsnlem  7128  ctssdclemn0  7139  ctssdc  7142  enumctlemm  7143  nnnninfeq  7156  nninfisollemne  7159  fodju0  7175  nninfwlpoimlemg  7203  nninfwlpoimlemginf  7204  iseqf1olemnab  10519  iseqf1olemab  10520  iseqf1olemqk  10525  iseqf1olemfvp  10528  seq3f1olemqsumkj  10529  seq3f1olemqsum  10531  seq3f1oleml  10534  seq3f1o  10535  fser0const  10547  expnnval  10554  2zsupmax  11266  2zinfmin  11283  xrmaxifle  11286  xrmaxiflemab  11287  xrmaxiflemlub  11288  xrmaxiflemcom  11289  summodclem3  11420  summodclem2a  11421  isum  11425  fsum3  11427  isumss  11431  fsumcl2lem  11438  fsumadd  11446  fsummulc2  11488  cvgratz  11572  prodmodclem3  11615  prodmodclem2a  11616  fprodseq  11623  prod1dc  11626  fprodmul  11631  ef0lem  11700  gcdval  11992  pcmpt  12375  pcmpt2  12376  ennnfonelemss  12461  ennnfonelemkh  12463  ennnfonelemhf1o  12464  fvprif  12819  mulgnn  13068  lgsdir2  14892  lgsne0  14897  bj-charfun  15017  bj-charfundc  15018  subctctexmid  15209  nninfsellemeq  15222  nninfsellemeqinf  15224  nninffeq  15228  dcapnconst  15268