Theorem iffalsed 3612

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1395  ifcif 3602

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 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-if 3603

This theorem is referenced by:  eqifdc  3639  ifnotdc  3641  ifandc  3643  mpodifsnif  6103  fimax2gtrilemstep  7071  updjudhcoinrg  7259  omp1eomlem  7272  difinfsnlem  7277  ctmlemr  7286  ctssdclemn0  7288  nnnninfeq  7306  nninfisol  7311  mkvprop  7336  nninfwlpoimlemg  7353  nninfwlpoimlemginf  7354  fzprval  10290  iseqf1olemnab  10735  iseqf1olemab  10736  iseqf1olemnanb  10737  iseqf1olemqk  10741  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  fser0const  10769  expnnval  10776  expnegap0  10781  ccatval2  11146  ccatalpha  11161  swrdnd  11206  swrd0g  11207  swrdccatin2  11276  2zsupmax  11752  2zinfmin  11769  xrmaxifle  11772  xrmaxiflemab  11773  xrmaxiflemlub  11774  xrmaxiflemcom  11775  xrmaxrecl  11781  sumrbdclem  11903  summodclem3  11906  isumss  11917  isumss2  11919  fsumadd  11932  fsumsplit  11933  sumsplitdc  11958  fsummulc2  11974  cvgratz  12058  prodrbdclem  12097  prodmodclem2a  12102  fprodntrivap  12110  prod1dc  12112  fprodmul  12117  fprodsplitdc  12122  ef0lem  12186  gcdval  12495  nninfctlemfo  12576  eucalgf  12592  eucalginv  12593  eucalglt  12594  pcmpt  12881  pcmpt2  12882  ennnfonelemjn  12988  ennnfonelemp1  12992  ennnfonelemhdmp1  12995  ennnfonelemss  12996  ennnfonelemkh  12998  ennnfonelemhf1o  12999  unct  13028  fvprif  13391  gsumfzz  13543  gsumfzcl  13547  mulgnn  13678  mulgnegnn  13684  gsumfzreidx  13889  gsumfzsubmcl  13890  gsumfzmptfidmadd  13891  gsumfzmhm  13895  znf1o  14630  dvexp2  15401  elply2  15424  ply1termlem  15431  dvply1  15454  lgsval2lem  15704  lgsval4  15714  lgsval4a  15716  lgsneg  15718  lgsneg1  15719  lgsdilem  15721  lgsdir  15729  lgsne0  15732  gausslemma2dlem1a  15752  gausslemma2dlem1f1o  15754  gausslemma2dlem3  15757  2lgslem3  15795  funvtxdm2domval  15845  funiedgdm2domval  15846  funvtxdm2vald  15847  funiedgdm2vald  15848  bj-charfun  16225  bj-charfundc  16226  2omap  16418  nnsf  16431  peano4nninf  16432  nninfsellemsuc  16438  nninfsellemeq  16440  nninffeq  16446  dceqnconst  16488