Theorem iffalsed 3619

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

Syntax hints:  ¬ wn 3   → 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:  eqifdc  3646  ifnotdc  3648  ifandc  3650  mpodifsnif  6124  fimax2gtrilemstep  7133  updjudhcoinrg  7323  omp1eomlem  7336  difinfsnlem  7341  ctmlemr  7350  ctssdclemn0  7352  nnnninfeq  7370  nninfisol  7375  mkvprop  7400  nninfwlpoimlemg  7417  nninfwlpoimlemginf  7418  fzprval  10360  iseqf1olemnab  10807  iseqf1olemab  10808  iseqf1olemnanb  10809  iseqf1olemqk  10813  seq3f1olemqsumkj  10817  seq3f1olemqsumk  10818  seq3f1olemqsum  10819  fser0const  10841  expnnval  10848  expnegap0  10853  ccatval2  11222  ccatalpha  11237  swrdnd  11287  swrd0g  11288  swrdccatin2  11357  2zsupmax  11847  2zinfmin  11864  xrmaxifle  11867  xrmaxiflemab  11868  xrmaxiflemlub  11869  xrmaxiflemcom  11870  xrmaxrecl  11876  sumrbdclem  11999  summodclem3  12002  isumss  12013  isumss2  12015  fsumadd  12028  fsumsplit  12029  sumsplitdc  12054  fsummulc2  12070  cvgratz  12154  prodrbdclem  12193  prodmodclem2a  12198  fprodntrivap  12206  prod1dc  12208  fprodmul  12213  fprodsplitdc  12218  ef0lem  12282  gcdval  12591  nninfctlemfo  12672  eucalgf  12688  eucalginv  12689  eucalglt  12690  pcmpt  12977  pcmpt2  12978  ennnfonelemjn  13084  ennnfonelemp1  13088  ennnfonelemhdmp1  13091  ennnfonelemss  13092  ennnfonelemkh  13094  ennnfonelemhf1o  13095  unct  13124  fvprif  13487  gsumfzz  13639  gsumfzcl  13643  mulgnn  13774  mulgnegnn  13780  gsumfzreidx  13985  gsumfzsubmcl  13986  gsumfzmptfidmadd  13987  gsumfzmhm  13991  znf1o  14727  dvexp2  15503  elply2  15526  ply1termlem  15533  dvply1  15556  lgsval2lem  15809  lgsval4  15819  lgsval4a  15821  lgsneg  15823  lgsneg1  15824  lgsdilem  15826  lgsdir  15834  lgsne0  15837  gausslemma2dlem1a  15857  gausslemma2dlem1f1o  15859  gausslemma2dlem3  15862  2lgslem3  15900  funvtxdm2domval  15950  funiedgdm2domval  15951  funvtxdm2vald  15952  funiedgdm2vald  15953  eupth2lem3lem4fi  16394  depindlem1  16427  bj-charfun  16503  bj-charfundc  16504  2omap  16695  nnsf  16711  peano4nninf  16712  nninfsellemsuc  16718  nninfsellemeq  16720  nninffeq  16726  dceqnconst  16773