Theorem iffalsed 3535

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 3533	. 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 1348   ifcif 3525

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 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-if 3526

This theorem is referenced by:  eqifdc  3559  ifnotdc  3561  ifandc  3562  mpodifsnif  5943  fimax2gtrilemstep  6874  updjudhcoinrg  7054  omp1eomlem  7067  difinfsnlem  7072  ctmlemr  7081  ctssdclemn0  7083  nnnninfeq  7100  nninfisol  7105  mkvprop  7130  fzprval  10025  iseqf1olemnab  10431  iseqf1olemab  10432  iseqf1olemnanb  10433  iseqf1olemqk  10437  seq3f1olemqsumkj  10441  seq3f1olemqsumk  10442  seq3f1olemqsum  10443  fser0const  10459  expnnval  10466  expnegap0  10471  2zsupmax  11176  2zinfmin  11193  xrmaxifle  11196  xrmaxiflemab  11197  xrmaxiflemlub  11198  xrmaxiflemcom  11199  xrmaxrecl  11205  sumrbdclem  11327  summodclem3  11330  isumss  11341  isumss2  11343  fsumadd  11356  fsumsplit  11357  sumsplitdc  11382  fsummulc2  11398  cvgratz  11482  prodrbdclem  11521  prodmodclem2a  11526  fprodntrivap  11534  prod1dc  11536  fprodmul  11541  fprodsplitdc  11546  ef0lem  11610  gcdval  11901  eucalgf  11996  eucalginv  11997  eucalglt  11998  pcmpt  12282  pcmpt2  12283  ennnfonelemjn  12344  ennnfonelemp1  12348  ennnfonelemhdmp1  12351  ennnfonelemss  12352  ennnfonelemkh  12354  ennnfonelemhf1o  12355  unct  12384  ressval2  12464  dvexp2  13391  lgsval2lem  13626  lgsval4  13636  lgsval4a  13638  lgsneg  13640  lgsneg1  13641  lgsdilem  13643  lgsdir  13651  lgsne0  13654  bj-charfun  13764  bj-charfundc  13765  nnsf  13960  peano4nninf  13961  nninfsellemsuc  13967  nninfsellemeq  13969  nninffeq  13975  dceqnconst  14013