Theorem iftrued 3633

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

Syntax hints:   → wi 4   = wceq 1398  ifcif 3624

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-if 3625

This theorem is referenced by:  ifeq2dadc  3658  eqifdc  3663  ifeqeqxdc  3673  mposnif  6155  fimax2gtrilemstep  7171  2omap  7282  updjudhcoinlf  7384  omp1eomlem  7398  difinfsnlem  7403  ctssdclemn0  7414  ctssdc  7417  enumctlemm  7418  nnnninfeq  7432  nninfisollemne  7435  fodju0  7451  nninfwlpoimlemg  7479  nninfwlpoimlemginf  7480  iseqf1olemnab  10887  iseqf1olemab  10888  iseqf1olemqk  10893  iseqf1olemfvp  10896  seq3f1olemqsumkj  10897  seq3f1olemqsum  10899  seq3f1oleml  10902  seq3f1o  10903  fser0const  10921  expnnval  10928  swrdval2  11368  swrdlend  11375  swrd0g  11377  2zsupmax  11936  2zinfmin  11953  xrmaxifle  11956  xrmaxiflemab  11957  xrmaxiflemlub  11958  xrmaxiflemcom  11959  summodclem3  12091  summodclem2a  12092  isum  12096  fsum3  12098  isumss  12102  fsumcl2lem  12109  fsumadd  12117  fsummulc2  12159  cvgratz  12243  prodmodclem3  12286  prodmodclem2a  12287  fprodseq  12294  prod1dc  12297  fprodmul  12302  ef0lem  12371  gcdval  12680  nninfctlemfo  12761  pcmpt  13066  pcmpt2  13067  ballotfilemsgt1  13198  ballotfilemsel1i  13200  ballotfilemsi  13202  ennnfonelemss  13245  ennnfonelemkh  13247  ennnfonelemhf1o  13248  fvprif  13640  gsumfzz  13792  gsumfzcl  13796  mulgnn  13927  gsumfzreidx  14138  gsumfzsubmcl  14139  gsumfzmptfidmadd  14140  gsumfzmhm  14144  znf1o  14911  dvply1  15742  lgsdir2  16018  lgsne0  16023  gausslemma2dlem1a  16043  gausslemma2dlem1f1o  16045  gausslemma2dlem2  16047  1loopgrvd2fi  16412  1hevtxdg1en  16415  eupth2lem3lem4fi  16580  bj-charfun  16689  bj-charfundc  16690  subctctexmid  16886  nninfsellemeq  16904  nninfsellemeqinf  16906  nninffeq  16910  dcapnconst  16959