Theorem iffalsed 3650

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1402  ifcif 3638

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-if 3639

This theorem is used by:  eqifdc  3677  ifnotdc  3679  ifandc  3681  ifeqeqxdc  3687  mpodifsnif  6184  fimax2gtrilemstep  7211  2omap  7324  updjudhcoinrg  7427  omp1eomlem  7440  difinfsnlem  7445  ctmlemr  7454  ctssdclemn0  7456  nnnninfeq  7474  nninfisol  7479  mkvprop  7504  nninfwlpoimlemg  7521  nninfwlpoimlemginf  7522  ind0  9310  fzprval  10505  iseqf1olemnab  10958  iseqf1olemab  10959  iseqf1olemnanb  10960  iseqf1olemqk  10964  seq3f1olemqsumkj  10968  seq3f1olemqsumk  10969  seq3f1olemqsum  10970  fser0const  10992  expnnval  10999  expnegap0  11004  ccatval2  11387  ccatalpha  11402  swrdnd  11452  swrd0g  11453  swrdccatin2  11522  2zsupmax  12014  2zinfmin  12033  xrmaxifle  12036  xrmaxiflemab  12037  xrmaxiflemlub  12038  xrmaxiflemcom  12039  xrmaxrecl  12045  sumrbdclem  12168  summodclem3  12171  isumss  12182  isumss2  12184  fsumadd  12197  fsumsplit  12198  sumsplitdc  12223  fsummulc2  12239  cvgratz  12323  prodrbdclem  12362  prodmodclem2a  12367  fprodntrivap  12375  prod1dc  12377  fprodmul  12382  fprodsplitdc  12387  ef0lem  12451  gcdval  12760  nninfctlemfo  12841  eucalgf  12857  eucalginv  12858  eucalglt  12859  pcmpt  13150  pcmpt2  13151  ballotfilemrv2  13322  ennnfonelemjn  13350  ennnfonelemp1  13354  ennnfonelemhdmp1  13357  ennnfonelemss  13358  ennnfonelemkh  13360  ennnfonelemhf1o  13361  unct  13390  fvprif  13722  gzsumcl  13862  mulgnn  13987  mulgnegnn  13993  gzsumreidx  14230  gzsumsubmcl  14231  gzsummhm  14234  znf1o  15094  psrlidmfi  15208  psrridmfi  15209  mvrf1fi  15219  mvrclfi  15226  dvexp2  15955  elply2  15978  ply1termlem  15985  dvply1  16008  bposlem5  16332  lgsval2lem  16351  lgsval4  16361  lgsval4a  16363  lgsneg  16365  lgsneg1  16366  lgsdilem  16368  lgsdir  16376  lgsne0  16379  gausslemma2dlem1a  16399  gausslemma2dlem1f1o  16401  gausslemma2dlem3  16404  2lgslem3  16442  funvtxdm2domval  16492  funiedgdm2domval  16493  funvtxdm2vald  16494  funiedgdm2vald  16495  eupth2lem3lem4fi  16936  depindlem1  16969  bj-charfun  17055  bj-charfundc  17056  idjudju  17269  nnsf  17271  peano4nninf  17272  nninfsellemsuc  17278  nninfsellemeq  17280  nninffeq  17286  dceqnconst  17334