Theorem iffalsed 3536

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1348  ifcif 3526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-if 3527

This theorem is referenced by:  eqifdc  3560  ifnotdc  3562  ifandc  3563  mpodifsnif  5946  fimax2gtrilemstep  6878  updjudhcoinrg  7058  omp1eomlem  7071  difinfsnlem  7076  ctmlemr  7085  ctssdclemn0  7087  nnnninfeq  7104  nninfisol  7109  mkvprop  7134  nninfwlpoimlemg  7151  nninfwlpoimlemginf  7152  fzprval  10038  iseqf1olemnab  10444  iseqf1olemab  10445  iseqf1olemnanb  10446  iseqf1olemqk  10450  seq3f1olemqsumkj  10454  seq3f1olemqsumk  10455  seq3f1olemqsum  10456  fser0const  10472  expnnval  10479  expnegap0  10484  2zsupmax  11189  2zinfmin  11206  xrmaxifle  11209  xrmaxiflemab  11210  xrmaxiflemlub  11211  xrmaxiflemcom  11212  xrmaxrecl  11218  sumrbdclem  11340  summodclem3  11343  isumss  11354  isumss2  11356  fsumadd  11369  fsumsplit  11370  sumsplitdc  11395  fsummulc2  11411  cvgratz  11495  prodrbdclem  11534  prodmodclem2a  11539  fprodntrivap  11547  prod1dc  11549  fprodmul  11554  fprodsplitdc  11559  ef0lem  11623  gcdval  11914  eucalgf  12009  eucalginv  12010  eucalglt  12011  pcmpt  12295  pcmpt2  12296  ennnfonelemjn  12357  ennnfonelemp1  12361  ennnfonelemhdmp1  12364  ennnfonelemss  12365  ennnfonelemkh  12367  ennnfonelemhf1o  12368  unct  12397  ressval2  12478  dvexp2  13470  lgsval2lem  13705  lgsval4  13715  lgsval4a  13717  lgsneg  13719  lgsneg1  13720  lgsdilem  13722  lgsdir  13730  lgsne0  13733  bj-charfun  13842  bj-charfundc  13843  nnsf  14038  peano4nninf  14039  nninfsellemsuc  14045  nninfsellemeq  14047  nninffeq  14053  dceqnconst  14091