Theorem iffalsed 3615

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1397  ifcif 3605

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 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-if 3606

This theorem is referenced by:  eqifdc  3642  ifnotdc  3644  ifandc  3646  mpodifsnif  6113  fimax2gtrilemstep  7089  updjudhcoinrg  7279  omp1eomlem  7292  difinfsnlem  7297  ctmlemr  7306  ctssdclemn0  7308  nnnninfeq  7326  nninfisol  7331  mkvprop  7356  nninfwlpoimlemg  7373  nninfwlpoimlemginf  7374  fzprval  10316  iseqf1olemnab  10762  iseqf1olemab  10763  iseqf1olemnanb  10764  iseqf1olemqk  10768  seq3f1olemqsumkj  10772  seq3f1olemqsumk  10773  seq3f1olemqsum  10774  fser0const  10796  expnnval  10803  expnegap0  10808  ccatval2  11174  ccatalpha  11189  swrdnd  11239  swrd0g  11240  swrdccatin2  11309  2zsupmax  11786  2zinfmin  11803  xrmaxifle  11806  xrmaxiflemab  11807  xrmaxiflemlub  11808  xrmaxiflemcom  11809  xrmaxrecl  11815  sumrbdclem  11937  summodclem3  11940  isumss  11951  isumss2  11953  fsumadd  11966  fsumsplit  11967  sumsplitdc  11992  fsummulc2  12008  cvgratz  12092  prodrbdclem  12131  prodmodclem2a  12136  fprodntrivap  12144  prod1dc  12146  fprodmul  12151  fprodsplitdc  12156  ef0lem  12220  gcdval  12529  nninfctlemfo  12610  eucalgf  12626  eucalginv  12627  eucalglt  12628  pcmpt  12915  pcmpt2  12916  ennnfonelemjn  13022  ennnfonelemp1  13026  ennnfonelemhdmp1  13029  ennnfonelemss  13030  ennnfonelemkh  13032  ennnfonelemhf1o  13033  unct  13062  fvprif  13425  gsumfzz  13577  gsumfzcl  13581  mulgnn  13712  mulgnegnn  13718  gsumfzreidx  13923  gsumfzsubmcl  13924  gsumfzmptfidmadd  13925  gsumfzmhm  13929  znf1o  14664  dvexp2  15435  elply2  15458  ply1termlem  15465  dvply1  15488  lgsval2lem  15738  lgsval4  15748  lgsval4a  15750  lgsneg  15752  lgsneg1  15753  lgsdilem  15755  lgsdir  15763  lgsne0  15766  gausslemma2dlem1a  15786  gausslemma2dlem1f1o  15788  gausslemma2dlem3  15791  2lgslem3  15829  funvtxdm2domval  15879  funiedgdm2domval  15880  funvtxdm2vald  15881  funiedgdm2vald  15882  bj-charfun  16402  bj-charfundc  16403  2omap  16594  nnsf  16607  peano4nninf  16608  nninfsellemsuc  16614  nninfsellemeq  16616  nninffeq  16622  dceqnconst  16664