Theorem iftrued 3609

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

Syntax hints:   → wi 4   = wceq 1395  ifcif 3602

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 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-if 3603

This theorem is referenced by:  ifeq2dadc  3634  eqifdc  3639  mposnif  6104  fimax2gtrilemstep  7070  updjudhcoinlf  7255  omp1eomlem  7269  difinfsnlem  7274  ctssdclemn0  7285  ctssdc  7288  enumctlemm  7289  nnnninfeq  7303  nninfisollemne  7306  fodju0  7322  nninfwlpoimlemg  7350  nninfwlpoimlemginf  7351  iseqf1olemnab  10731  iseqf1olemab  10732  iseqf1olemqk  10737  iseqf1olemfvp  10740  seq3f1olemqsumkj  10741  seq3f1olemqsum  10743  seq3f1oleml  10746  seq3f1o  10747  fser0const  10765  expnnval  10772  swrdval2  11191  swrdlend  11198  swrd0g  11200  2zsupmax  11745  2zinfmin  11762  xrmaxifle  11765  xrmaxiflemab  11766  xrmaxiflemlub  11767  xrmaxiflemcom  11768  summodclem3  11899  summodclem2a  11900  isum  11904  fsum3  11906  isumss  11910  fsumcl2lem  11917  fsumadd  11925  fsummulc2  11967  cvgratz  12051  prodmodclem3  12094  prodmodclem2a  12095  fprodseq  12102  prod1dc  12105  fprodmul  12110  ef0lem  12179  gcdval  12488  nninfctlemfo  12569  pcmpt  12874  pcmpt2  12875  ennnfonelemss  12989  ennnfonelemkh  12991  ennnfonelemhf1o  12992  fvprif  13384  gsumfzz  13536  gsumfzcl  13540  mulgnn  13671  gsumfzreidx  13882  gsumfzsubmcl  13883  gsumfzmptfidmadd  13884  gsumfzmhm  13888  znf1o  14623  dvply1  15447  lgsdir2  15720  lgsne0  15725  gausslemma2dlem1a  15745  gausslemma2dlem1f1o  15747  gausslemma2dlem2  15749  bj-charfun  16194  bj-charfundc  16195  2omap  16388  subctctexmid  16395  nninfsellemeq  16410  nninfsellemeqinf  16412  nninffeq  16416  dcapnconst  16459