Theorem iftrued 3616

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

Syntax hints:   → wi 4   = wceq 1398  ifcif 3607

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-if 3608

This theorem is referenced by:  ifeq2dadc  3641  eqifdc  3646  mposnif  6125  fimax2gtrilemstep  7133  updjudhcoinlf  7322  omp1eomlem  7336  difinfsnlem  7341  ctssdclemn0  7352  ctssdc  7355  enumctlemm  7356  nnnninfeq  7370  nninfisollemne  7373  fodju0  7389  nninfwlpoimlemg  7417  nninfwlpoimlemginf  7418  iseqf1olemnab  10807  iseqf1olemab  10808  iseqf1olemqk  10813  iseqf1olemfvp  10816  seq3f1olemqsumkj  10817  seq3f1olemqsum  10819  seq3f1oleml  10822  seq3f1o  10823  fser0const  10841  expnnval  10848  swrdval2  11279  swrdlend  11286  swrd0g  11288  2zsupmax  11847  2zinfmin  11864  xrmaxifle  11867  xrmaxiflemab  11868  xrmaxiflemlub  11869  xrmaxiflemcom  11870  summodclem3  12002  summodclem2a  12003  isum  12007  fsum3  12009  isumss  12013  fsumcl2lem  12020  fsumadd  12028  fsummulc2  12070  cvgratz  12154  prodmodclem3  12197  prodmodclem2a  12198  fprodseq  12205  prod1dc  12208  fprodmul  12213  ef0lem  12282  gcdval  12591  nninfctlemfo  12672  pcmpt  12977  pcmpt2  12978  ennnfonelemss  13092  ennnfonelemkh  13094  ennnfonelemhf1o  13095  fvprif  13487  gsumfzz  13639  gsumfzcl  13643  mulgnn  13774  gsumfzreidx  13985  gsumfzsubmcl  13986  gsumfzmptfidmadd  13987  gsumfzmhm  13991  znf1o  14727  dvply1  15556  lgsdir2  15832  lgsne0  15837  gausslemma2dlem1a  15857  gausslemma2dlem1f1o  15859  gausslemma2dlem2  15861  1loopgrvd2fi  16226  1hevtxdg1en  16229  eupth2lem3lem4fi  16394  bj-charfun  16503  bj-charfundc  16504  2omap  16695  subctctexmid  16702  nninfsellemeq  16720  nninfsellemeqinf  16722  nninffeq  16726  dcapnconst  16774