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  6114  fimax2gtrilemstep  7090  updjudhcoinrg  7280  omp1eomlem  7293  difinfsnlem  7298  ctmlemr  7307  ctssdclemn0  7309  nnnninfeq  7327  nninfisol  7332  mkvprop  7357  nninfwlpoimlemg  7374  nninfwlpoimlemginf  7375  fzprval  10317  iseqf1olemnab  10764  iseqf1olemab  10765  iseqf1olemnanb  10766  iseqf1olemqk  10770  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  fser0const  10798  expnnval  10805  expnegap0  10810  ccatval2  11179  ccatalpha  11194  swrdnd  11244  swrd0g  11245  swrdccatin2  11314  2zsupmax  11791  2zinfmin  11808  xrmaxifle  11811  xrmaxiflemab  11812  xrmaxiflemlub  11813  xrmaxiflemcom  11814  xrmaxrecl  11820  sumrbdclem  11943  summodclem3  11946  isumss  11957  isumss2  11959  fsumadd  11972  fsumsplit  11973  sumsplitdc  11998  fsummulc2  12014  cvgratz  12098  prodrbdclem  12137  prodmodclem2a  12142  fprodntrivap  12150  prod1dc  12152  fprodmul  12157  fprodsplitdc  12162  ef0lem  12226  gcdval  12535  nninfctlemfo  12616  eucalgf  12632  eucalginv  12633  eucalglt  12634  pcmpt  12921  pcmpt2  12922  ennnfonelemjn  13028  ennnfonelemp1  13032  ennnfonelemhdmp1  13035  ennnfonelemss  13036  ennnfonelemkh  13038  ennnfonelemhf1o  13039  unct  13068  fvprif  13431  gsumfzz  13583  gsumfzcl  13587  mulgnn  13718  mulgnegnn  13724  gsumfzreidx  13929  gsumfzsubmcl  13930  gsumfzmptfidmadd  13931  gsumfzmhm  13935  znf1o  14671  dvexp2  15442  elply2  15465  ply1termlem  15472  dvply1  15495  lgsval2lem  15745  lgsval4  15755  lgsval4a  15757  lgsneg  15759  lgsneg1  15760  lgsdilem  15762  lgsdir  15770  lgsne0  15773  gausslemma2dlem1a  15793  gausslemma2dlem1f1o  15795  gausslemma2dlem3  15798  2lgslem3  15836  funvtxdm2domval  15886  funiedgdm2domval  15887  funvtxdm2vald  15888  funiedgdm2vald  15889  eupth2lem3lem4fi  16330  depindlem1  16351  bj-charfun  16428  bj-charfundc  16429  2omap  16620  nnsf  16633  peano4nninf  16634  nninfsellemsuc  16640  nninfsellemeq  16642  nninffeq  16648  dceqnconst  16691