Theorem iffalsed 3401

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1289  ifcif 3391

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-if 3392

This theorem is referenced by:  eqifdc  3423  ifandc  3425  fimax2gtrilemstep  6606  updjudhcoinrg  6762  fzprval  9484  iseqf1olemnab  9905  iseqf1olemab  9906  iseqf1olemnanb  9907  iseqf1olemqk  9911  seq3f1olemqsumkj  9915  seq3f1olemqsumk  9916  seq3f1olemqsum  9917  fser0const  9939  expnnval  9946  expnegap0  9951  isumrblem  10752  isummolem3  10757  isumss  10770  isumss2  10772  fsumadd  10787  fsumsplit  10788  sumsplitdc  10813  fsummulc2  10829  cvgratz  10913  ef0lem  10937  gcdval  11216  eucalgf  11302  eucalginv  11303  eucalglt  11304  nnsf  11778  peano4nninf  11779  nninfalllemn  11781  nninfsellemsuc  11787  nninfsellemeq  11789