Theorem iffalsed 3544

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 3542	. 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 1353   ifcif 3534

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 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-if 3535

This theorem is referenced by:  eqifdc  3569  ifnotdc  3571  ifandc  3572  mpodifsnif  5967  fimax2gtrilemstep  6899  updjudhcoinrg  7079  omp1eomlem  7092  difinfsnlem  7097  ctmlemr  7106  ctssdclemn0  7108  nnnninfeq  7125  nninfisol  7130  mkvprop  7155  nninfwlpoimlemg  7172  nninfwlpoimlemginf  7173  fzprval  10079  iseqf1olemnab  10485  iseqf1olemab  10486  iseqf1olemnanb  10487  iseqf1olemqk  10491  seq3f1olemqsumkj  10495  seq3f1olemqsumk  10496  seq3f1olemqsum  10497  fser0const  10513  expnnval  10520  expnegap0  10525  2zsupmax  11229  2zinfmin  11246  xrmaxifle  11249  xrmaxiflemab  11250  xrmaxiflemlub  11251  xrmaxiflemcom  11252  xrmaxrecl  11258  sumrbdclem  11380  summodclem3  11383  isumss  11394  isumss2  11396  fsumadd  11409  fsumsplit  11410  sumsplitdc  11435  fsummulc2  11451  cvgratz  11535  prodrbdclem  11574  prodmodclem2a  11579  fprodntrivap  11587  prod1dc  11589  fprodmul  11594  fprodsplitdc  11599  ef0lem  11663  gcdval  11954  eucalgf  12049  eucalginv  12050  eucalglt  12051  pcmpt  12335  pcmpt2  12336  ennnfonelemjn  12397  ennnfonelemp1  12401  ennnfonelemhdmp1  12404  ennnfonelemss  12405  ennnfonelemkh  12407  ennnfonelemhf1o  12408  unct  12437  mulgnn  12943  mulgnegnn  12947  dvexp2  14069  lgsval2lem  14304  lgsval4  14314  lgsval4a  14316  lgsneg  14318  lgsneg1  14319  lgsdilem  14321  lgsdir  14329  lgsne0  14332  bj-charfun  14441  bj-charfundc  14442  nnsf  14636  peano4nninf  14637  nninfsellemsuc  14643  nninfsellemeq  14645  nninffeq  14651  dceqnconst  14689