Theorem iffalsed 3613

Description: Value of the conditional operator when its first argument is false. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypothesis

Ref	Expression
iffalsed.1	⊢ (𝜑 → ¬ 𝜒)

Assertion

Ref	Expression
iffalsed	⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐵)

Proof of Theorem iffalsed

Step	Hyp	Ref	Expression
1		iffalsed.1	. 2 ⊢ (𝜑 → ¬ 𝜒)
2		iffalse 3611	. 2 ⊢ (¬ 𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐵)
3	1, 2	syl 14	1 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1395  ifcif 3603

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 3604

This theorem is referenced by:  eqifdc  3640  ifnotdc  3642  ifandc  3644  mpodifsnif  6109  fimax2gtrilemstep  7083  updjudhcoinrg  7271  omp1eomlem  7284  difinfsnlem  7289  ctmlemr  7298  ctssdclemn0  7300  nnnninfeq  7318  nninfisol  7323  mkvprop  7348  nninfwlpoimlemg  7365  nninfwlpoimlemginf  7366  fzprval  10307  iseqf1olemnab  10753  iseqf1olemab  10754  iseqf1olemnanb  10755  iseqf1olemqk  10759  seq3f1olemqsumkj  10763  seq3f1olemqsumk  10764  seq3f1olemqsum  10765  fser0const  10787  expnnval  10794  expnegap0  10799  ccatval2  11165  ccatalpha  11180  swrdnd  11230  swrd0g  11231  swrdccatin2  11300  2zsupmax  11777  2zinfmin  11794  xrmaxifle  11797  xrmaxiflemab  11798  xrmaxiflemlub  11799  xrmaxiflemcom  11800  xrmaxrecl  11806  sumrbdclem  11928  summodclem3  11931  isumss  11942  isumss2  11944  fsumadd  11957  fsumsplit  11958  sumsplitdc  11983  fsummulc2  11999  cvgratz  12083  prodrbdclem  12122  prodmodclem2a  12127  fprodntrivap  12135  prod1dc  12137  fprodmul  12142  fprodsplitdc  12147  ef0lem  12211  gcdval  12520  nninfctlemfo  12601  eucalgf  12617  eucalginv  12618  eucalglt  12619  pcmpt  12906  pcmpt2  12907  ennnfonelemjn  13013  ennnfonelemp1  13017  ennnfonelemhdmp1  13020  ennnfonelemss  13021  ennnfonelemkh  13023  ennnfonelemhf1o  13024  unct  13053  fvprif  13416  gsumfzz  13568  gsumfzcl  13572  mulgnn  13703  mulgnegnn  13709  gsumfzreidx  13914  gsumfzsubmcl  13915  gsumfzmptfidmadd  13916  gsumfzmhm  13920  znf1o  14655  dvexp2  15426  elply2  15449  ply1termlem  15456  dvply1  15479  lgsval2lem  15729  lgsval4  15739  lgsval4a  15741  lgsneg  15743  lgsneg1  15744  lgsdilem  15746  lgsdir  15754  lgsne0  15757  gausslemma2dlem1a  15777  gausslemma2dlem1f1o  15779  gausslemma2dlem3  15782  2lgslem3  15820  funvtxdm2domval  15870  funiedgdm2domval  15871  funvtxdm2vald  15872  funiedgdm2vald  15873  bj-charfun  16338  bj-charfundc  16339  2omap  16530  nnsf  16543  peano4nninf  16544  nninfsellemsuc  16550  nninfsellemeq  16552  nninffeq  16558  dceqnconst  16600