Theorem iffalsed 3546

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1353  ifcif 3536

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 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-if 3537

This theorem is referenced by:  eqifdc  3571  ifnotdc  3573  ifandc  3574  mpodifsnif  5970  fimax2gtrilemstep  6902  updjudhcoinrg  7082  omp1eomlem  7095  difinfsnlem  7100  ctmlemr  7109  ctssdclemn0  7111  nnnninfeq  7128  nninfisol  7133  mkvprop  7158  nninfwlpoimlemg  7175  nninfwlpoimlemginf  7176  fzprval  10084  iseqf1olemnab  10490  iseqf1olemab  10491  iseqf1olemnanb  10492  iseqf1olemqk  10496  seq3f1olemqsumkj  10500  seq3f1olemqsumk  10501  seq3f1olemqsum  10502  fser0const  10518  expnnval  10525  expnegap0  10530  2zsupmax  11236  2zinfmin  11253  xrmaxifle  11256  xrmaxiflemab  11257  xrmaxiflemlub  11258  xrmaxiflemcom  11259  xrmaxrecl  11265  sumrbdclem  11387  summodclem3  11390  isumss  11401  isumss2  11403  fsumadd  11416  fsumsplit  11417  sumsplitdc  11442  fsummulc2  11458  cvgratz  11542  prodrbdclem  11581  prodmodclem2a  11586  fprodntrivap  11594  prod1dc  11596  fprodmul  11601  fprodsplitdc  11606  ef0lem  11670  gcdval  11962  eucalgf  12057  eucalginv  12058  eucalglt  12059  pcmpt  12343  pcmpt2  12344  ennnfonelemjn  12405  ennnfonelemp1  12409  ennnfonelemhdmp1  12412  ennnfonelemss  12413  ennnfonelemkh  12415  ennnfonelemhf1o  12416  unct  12445  fvprif  12767  mulgnn  12994  mulgnegnn  12998  dvexp2  14261  lgsval2lem  14496  lgsval4  14506  lgsval4a  14508  lgsneg  14510  lgsneg1  14511  lgsdilem  14513  lgsdir  14521  lgsne0  14524  bj-charfun  14644  bj-charfundc  14645  nnsf  14839  peano4nninf  14840  nninfsellemsuc  14846  nninfsellemeq  14848  nninffeq  14854  dceqnconst  14893