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  6181  fimax2gtrilemstep  7205  2omap  7319  updjudhcoinrg  7422  omp1eomlem  7435  difinfsnlem  7440  ctmlemr  7449  ctssdclemn0  7451  nnnninfeq  7469  nninfisol  7474  mkvprop  7499  nninfwlpoimlemg  7516  nninfwlpoimlemginf  7517  ind0  9304  fzprval  10500  iseqf1olemnab  10953  iseqf1olemab  10954  iseqf1olemnanb  10955  iseqf1olemqk  10959  seq3f1olemqsumkj  10963  seq3f1olemqsumk  10964  seq3f1olemqsum  10965  fser0const  10987  expnnval  10994  expnegap0  10999  ccatval2  11382  ccatalpha  11397  swrdnd  11447  swrd0g  11448  swrdccatin2  11517  2zsupmax  12009  2zinfmin  12028  xrmaxifle  12031  xrmaxiflemab  12032  xrmaxiflemlub  12033  xrmaxiflemcom  12034  xrmaxrecl  12040  sumrbdclem  12163  summodclem3  12166  isumss  12177  isumss2  12179  fsumadd  12192  fsumsplit  12193  sumsplitdc  12218  fsummulc2  12234  cvgratz  12318  prodrbdclem  12357  prodmodclem2a  12362  fprodntrivap  12370  prod1dc  12372  fprodmul  12377  fprodsplitdc  12382  ef0lem  12446  gcdval  12755  nninfctlemfo  12836  eucalgf  12852  eucalginv  12853  eucalglt  12854  pcmpt  13145  pcmpt2  13146  ballotfilemrv2  13317  ennnfonelemjn  13345  ennnfonelemp1  13349  ennnfonelemhdmp1  13352  ennnfonelemss  13353  ennnfonelemkh  13355  ennnfonelemhf1o  13356  unct  13385  fvprif  13717  gzsumcl  13857  mulgnn  13982  mulgnegnn  13988  gzsumreidx  14225  gzsumsubmcl  14226  gzsummhm  14229  znf1o  15070  dvexp2  15904  elply2  15927  ply1termlem  15934  dvply1  15957  bposlem5  16276  lgsval2lem  16295  lgsval4  16305  lgsval4a  16307  lgsneg  16309  lgsneg1  16310  lgsdilem  16312  lgsdir  16320  lgsne0  16323  gausslemma2dlem1a  16343  gausslemma2dlem1f1o  16345  gausslemma2dlem3  16348  2lgslem3  16386  funvtxdm2domval  16436  funiedgdm2domval  16437  funvtxdm2vald  16438  funiedgdm2vald  16439  eupth2lem3lem4fi  16880  depindlem1  16913  bj-charfun  16999  bj-charfundc  17000  nnsf  17214  peano4nninf  17215  nninfsellemsuc  17221  nninfsellemeq  17223  nninffeq  17229  dceqnconst  17277