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  7318  updjudhcoinrg  7421  omp1eomlem  7434  difinfsnlem  7439  ctmlemr  7448  ctssdclemn0  7450  nnnninfeq  7468  nninfisol  7473  mkvprop  7498  nninfwlpoimlemg  7515  nninfwlpoimlemginf  7516  ind0  9303  fzprval  10499  iseqf1olemnab  10951  iseqf1olemab  10952  iseqf1olemnanb  10953  iseqf1olemqk  10957  seq3f1olemqsumkj  10961  seq3f1olemqsumk  10962  seq3f1olemqsum  10963  fser0const  10985  expnnval  10992  expnegap0  10997  ccatval2  11380  ccatalpha  11395  swrdnd  11445  swrd0g  11446  swrdccatin2  11515  2zsupmax  12007  2zinfmin  12025  xrmaxifle  12028  xrmaxiflemab  12029  xrmaxiflemlub  12030  xrmaxiflemcom  12031  xrmaxrecl  12037  sumrbdclem  12160  summodclem3  12163  isumss  12174  isumss2  12176  fsumadd  12189  fsumsplit  12190  sumsplitdc  12215  fsummulc2  12231  cvgratz  12315  prodrbdclem  12354  prodmodclem2a  12359  fprodntrivap  12367  prod1dc  12369  fprodmul  12374  fprodsplitdc  12379  ef0lem  12443  gcdval  12752  nninfctlemfo  12833  eucalgf  12849  eucalginv  12850  eucalglt  12851  pcmpt  13142  pcmpt2  13143  ballotfilemrv2  13314  ennnfonelemjn  13342  ennnfonelemp1  13346  ennnfonelemhdmp1  13349  ennnfonelemss  13350  ennnfonelemkh  13352  ennnfonelemhf1o  13353  unct  13382  fvprif  13713  gzsumcl  13853  mulgnn  13978  mulgnegnn  13984  gzsumreidx  14190  gzsumsubmcl  14191  gzsummhm  14194  znf1o  15035  dvexp2  15862  elply2  15885  ply1termlem  15892  dvply1  15915  bposlem5  16213  lgsval2lem  16227  lgsval4  16237  lgsval4a  16239  lgsneg  16241  lgsneg1  16242  lgsdilem  16244  lgsdir  16252  lgsne0  16255  gausslemma2dlem1a  16275  gausslemma2dlem1f1o  16277  gausslemma2dlem3  16280  2lgslem3  16318  funvtxdm2domval  16368  funiedgdm2domval  16369  funvtxdm2vald  16370  funiedgdm2vald  16371  eupth2lem3lem4fi  16812  depindlem1  16845  bj-charfun  16931  bj-charfundc  16932  nnsf  17146  peano4nninf  17147  nninfsellemsuc  17153  nninfsellemeq  17155  nninffeq  17161  dceqnconst  17208