Theorem iffalsed 3632

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1398  ifcif 3620

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-if 3621

This theorem is referenced by:  eqifdc  3659  ifnotdc  3661  ifandc  3663  mpodifsnif  6146  fimax2gtrilemstep  7158  2omap  7269  updjudhcoinrg  7372  omp1eomlem  7385  difinfsnlem  7390  ctmlemr  7399  ctssdclemn0  7401  nnnninfeq  7419  nninfisol  7424  mkvprop  7449  nninfwlpoimlemg  7466  nninfwlpoimlemginf  7467  fzprval  10416  iseqf1olemnab  10863  iseqf1olemab  10864  iseqf1olemnanb  10865  iseqf1olemqk  10869  seq3f1olemqsumkj  10873  seq3f1olemqsumk  10874  seq3f1olemqsum  10875  fser0const  10897  expnnval  10904  expnegap0  10909  ccatval2  11286  ccatalpha  11301  swrdnd  11351  swrd0g  11352  swrdccatin2  11421  2zsupmax  11911  2zinfmin  11928  xrmaxifle  11931  xrmaxiflemab  11932  xrmaxiflemlub  11933  xrmaxiflemcom  11934  xrmaxrecl  11940  sumrbdclem  12063  summodclem3  12066  isumss  12077  isumss2  12079  fsumadd  12092  fsumsplit  12093  sumsplitdc  12118  fsummulc2  12134  cvgratz  12218  prodrbdclem  12257  prodmodclem2a  12262  fprodntrivap  12270  prod1dc  12272  fprodmul  12277  fprodsplitdc  12282  ef0lem  12346  gcdval  12655  nninfctlemfo  12736  eucalgf  12752  eucalginv  12753  eucalglt  12754  pcmpt  13041  pcmpt2  13042  ennnfonelemjn  13153  ennnfonelemp1  13157  ennnfonelemhdmp1  13160  ennnfonelemss  13161  ennnfonelemkh  13163  ennnfonelemhf1o  13164  unct  13193  fvprif  13556  gsumfzz  13708  gsumfzcl  13712  mulgnn  13843  mulgnegnn  13849  gsumfzreidx  14054  gsumfzsubmcl  14055  gsumfzmptfidmadd  14056  gsumfzmhm  14060  znf1o  14799  dvexp2  15577  elply2  15600  ply1termlem  15607  dvply1  15630  lgsval2lem  15883  lgsval4  15893  lgsval4a  15895  lgsneg  15897  lgsneg1  15898  lgsdilem  15900  lgsdir  15908  lgsne0  15911  gausslemma2dlem1a  15931  gausslemma2dlem1f1o  15933  gausslemma2dlem3  15936  2lgslem3  15974  funvtxdm2domval  16024  funiedgdm2domval  16025  funvtxdm2vald  16026  funiedgdm2vald  16027  eupth2lem3lem4fi  16468  depindlem1  16501  bj-charfun  16577  bj-charfundc  16578  nnsf  16783  peano4nninf  16784  nninfsellemsuc  16790  nninfsellemeq  16792  nninffeq  16798  dceqnconst  16846