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  6089  fimax2gtrilemstep  7050  updjudhcoinlf  7235  omp1eomlem  7249  difinfsnlem  7254  ctssdclemn0  7265  ctssdc  7268  enumctlemm  7269  nnnninfeq  7283  nninfisollemne  7286  fodju0  7302  nninfwlpoimlemg  7330  nninfwlpoimlemginf  7331  iseqf1olemnab  10710  iseqf1olemab  10711  iseqf1olemqk  10716  iseqf1olemfvp  10719  seq3f1olemqsumkj  10720  seq3f1olemqsum  10722  seq3f1oleml  10725  seq3f1o  10726  fser0const  10744  expnnval  10751  swrdval2  11169  swrdlend  11176  swrd0g  11178  2zsupmax  11723  2zinfmin  11740  xrmaxifle  11743  xrmaxiflemab  11744  xrmaxiflemlub  11745  xrmaxiflemcom  11746  summodclem3  11877  summodclem2a  11878  isum  11882  fsum3  11884  isumss  11888  fsumcl2lem  11895  fsumadd  11903  fsummulc2  11945  cvgratz  12029  prodmodclem3  12072  prodmodclem2a  12073  fprodseq  12080  prod1dc  12083  fprodmul  12088  ef0lem  12157  gcdval  12466  nninfctlemfo  12547  pcmpt  12852  pcmpt2  12853  ennnfonelemss  12967  ennnfonelemkh  12969  ennnfonelemhf1o  12970  fvprif  13362  gsumfzz  13514  gsumfzcl  13518  mulgnn  13649  gsumfzreidx  13860  gsumfzsubmcl  13861  gsumfzmptfidmadd  13862  gsumfzmhm  13866  znf1o  14600  dvply1  15424  lgsdir2  15697  lgsne0  15702  gausslemma2dlem1a  15722  gausslemma2dlem1f1o  15724  gausslemma2dlem2  15726  bj-charfun  16100  bj-charfundc  16101  2omap  16290  subctctexmid  16297  nninfsellemeq  16311  nninfsellemeqinf  16313  nninffeq  16317  dcapnconst  16360