Theorem iffalsed 3581

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 3579	. 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 1373   ifcif 3571

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-if 3572

This theorem is referenced by:  eqifdc  3607  ifnotdc  3609  ifandc  3610  mpodifsnif  6038  fimax2gtrilemstep  6997  updjudhcoinrg  7183  omp1eomlem  7196  difinfsnlem  7201  ctmlemr  7210  ctssdclemn0  7212  nnnninfeq  7230  nninfisol  7235  mkvprop  7260  nninfwlpoimlemg  7277  nninfwlpoimlemginf  7278  fzprval  10204  iseqf1olemnab  10646  iseqf1olemab  10647  iseqf1olemnanb  10648  iseqf1olemqk  10652  seq3f1olemqsumkj  10656  seq3f1olemqsumk  10657  seq3f1olemqsum  10658  fser0const  10680  expnnval  10687  expnegap0  10692  ccatval2  11054  swrdnd  11112  swrd0g  11113  2zsupmax  11537  2zinfmin  11554  xrmaxifle  11557  xrmaxiflemab  11558  xrmaxiflemlub  11559  xrmaxiflemcom  11560  xrmaxrecl  11566  sumrbdclem  11688  summodclem3  11691  isumss  11702  isumss2  11704  fsumadd  11717  fsumsplit  11718  sumsplitdc  11743  fsummulc2  11759  cvgratz  11843  prodrbdclem  11882  prodmodclem2a  11887  fprodntrivap  11895  prod1dc  11897  fprodmul  11902  fprodsplitdc  11907  ef0lem  11971  gcdval  12280  nninfctlemfo  12361  eucalgf  12377  eucalginv  12378  eucalglt  12379  pcmpt  12666  pcmpt2  12667  ennnfonelemjn  12773  ennnfonelemp1  12777  ennnfonelemhdmp1  12780  ennnfonelemss  12781  ennnfonelemkh  12783  ennnfonelemhf1o  12784  unct  12813  fvprif  13175  gsumfzz  13327  gsumfzcl  13331  mulgnn  13462  mulgnegnn  13468  gsumfzreidx  13673  gsumfzsubmcl  13674  gsumfzmptfidmadd  13675  gsumfzmhm  13679  znf1o  14413  dvexp2  15184  elply2  15207  ply1termlem  15214  dvply1  15237  lgsval2lem  15487  lgsval4  15497  lgsval4a  15499  lgsneg  15501  lgsneg1  15502  lgsdilem  15504  lgsdir  15512  lgsne0  15515  gausslemma2dlem1a  15535  gausslemma2dlem1f1o  15537  gausslemma2dlem3  15540  2lgslem3  15578  funvtxdm2domval  15626  funiedgdm2domval  15627  funvtxdm2vald  15628  funiedgdm2vald  15629  bj-charfun  15743  bj-charfundc  15744  2omap  15932  nnsf  15942  peano4nninf  15943  nninfsellemsuc  15949  nninfsellemeq  15951  nninffeq  15957  dceqnconst  15999