Theorem iffalsed 3525

Description: Value of the conditional operator when its first argument is false. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypothesis

Ref	Expression
iffalsed.1	|- ( ph -> -. ch )

Assertion

Ref	Expression
iffalsed	|- ( ph -> if ( ch , A , B ) = B )

Proof of Theorem iffalsed

Step	Hyp	Ref	Expression
1		iffalsed.1	. 2 |- ( ph -> -. ch )
2		iffalse 3523	. 2 |- ( -. ch -> if ( ch , A , B ) = B )
3	1, 2	syl 14	1 |- ( ph -> if ( ch , A , B ) = B )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1342   ifcif 3515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-11 1493  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-if 3516

This theorem is referenced by:  eqifdc  3549  ifandc  3551  mpodifsnif  5926  fimax2gtrilemstep  6857  updjudhcoinrg  7037  omp1eomlem  7050  difinfsnlem  7055  ctmlemr  7064  ctssdclemn0  7066  nnnninfeq  7083  nninfisol  7088  mkvprop  7113  fzprval  10007  iseqf1olemnab  10413  iseqf1olemab  10414  iseqf1olemnanb  10415  iseqf1olemqk  10419  seq3f1olemqsumkj  10423  seq3f1olemqsumk  10424  seq3f1olemqsum  10425  fser0const  10441  expnnval  10448  expnegap0  10453  2zsupmax  11153  2zinfmin  11170  xrmaxifle  11173  xrmaxiflemab  11174  xrmaxiflemlub  11175  xrmaxiflemcom  11176  xrmaxrecl  11182  sumrbdclem  11304  summodclem3  11307  isumss  11318  isumss2  11320  fsumadd  11333  fsumsplit  11334  sumsplitdc  11359  fsummulc2  11375  cvgratz  11459  prodrbdclem  11498  prodmodclem2a  11503  fprodntrivap  11511  prod1dc  11513  fprodmul  11518  fprodsplitdc  11523  ef0lem  11587  gcdval  11877  eucalgf  11966  eucalginv  11967  eucalglt  11968  pcmpt  12250  pcmpt2  12251  ennnfonelemjn  12272  ennnfonelemp1  12276  ennnfonelemhdmp1  12279  ennnfonelemss  12280  ennnfonelemkh  12282  ennnfonelemhf1o  12283  unct  12312  ressval2  12391  dvexp2  13217  bj-charfun  13524  bj-charfundc  13525  nnsf  13719  peano4nninf  13720  nninfsellemsuc  13726  nninfsellemeq  13728  nninffeq  13734  dceqnconst  13772