Theorem iffalsed 3567

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 3565	. 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 1364   ifcif 3557

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 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-if 3558

This theorem is referenced by:  eqifdc  3592  ifnotdc  3594  ifandc  3595  mpodifsnif  6011  fimax2gtrilemstep  6956  updjudhcoinrg  7140  omp1eomlem  7153  difinfsnlem  7158  ctmlemr  7167  ctssdclemn0  7169  nnnninfeq  7187  nninfisol  7192  mkvprop  7217  nninfwlpoimlemg  7234  nninfwlpoimlemginf  7235  fzprval  10148  iseqf1olemnab  10572  iseqf1olemab  10573  iseqf1olemnanb  10574  iseqf1olemqk  10578  seq3f1olemqsumkj  10582  seq3f1olemqsumk  10583  seq3f1olemqsum  10584  fser0const  10606  expnnval  10613  expnegap0  10618  2zsupmax  11369  2zinfmin  11386  xrmaxifle  11389  xrmaxiflemab  11390  xrmaxiflemlub  11391  xrmaxiflemcom  11392  xrmaxrecl  11398  sumrbdclem  11520  summodclem3  11523  isumss  11534  isumss2  11536  fsumadd  11549  fsumsplit  11550  sumsplitdc  11575  fsummulc2  11591  cvgratz  11675  prodrbdclem  11714  prodmodclem2a  11719  fprodntrivap  11727  prod1dc  11729  fprodmul  11734  fprodsplitdc  11739  ef0lem  11803  gcdval  12096  nninfctlemfo  12177  eucalgf  12193  eucalginv  12194  eucalglt  12195  pcmpt  12481  pcmpt2  12482  ennnfonelemjn  12559  ennnfonelemp1  12563  ennnfonelemhdmp1  12566  ennnfonelemss  12567  ennnfonelemkh  12569  ennnfonelemhf1o  12570  unct  12599  fvprif  12926  gsumfzz  13067  gsumfzcl  13071  mulgnn  13196  mulgnegnn  13202  gsumfzreidx  13407  gsumfzsubmcl  13408  gsumfzmptfidmadd  13409  gsumfzmhm  13413  znf1o  14139  dvexp2  14861  elply2  14881  ply1termlem  14888  lgsval2lem  15126  lgsval4  15136  lgsval4a  15138  lgsneg  15140  lgsneg1  15141  lgsdilem  15143  lgsdir  15151  lgsne0  15154  gausslemma2dlem1a  15174  gausslemma2dlem1f1o  15176  gausslemma2dlem3  15179  bj-charfun  15299  bj-charfundc  15300  nnsf  15495  peano4nninf  15496  nninfsellemsuc  15502  nninfsellemeq  15504  nninffeq  15510  dceqnconst  15550