Theorem iffalsed 3572

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 3570	. 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 3562

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-if 3563

This theorem is referenced by:  eqifdc  3597  ifnotdc  3599  ifandc  3600  mpodifsnif  6019  fimax2gtrilemstep  6970  updjudhcoinrg  7156  omp1eomlem  7169  difinfsnlem  7174  ctmlemr  7183  ctssdclemn0  7185  nnnninfeq  7203  nninfisol  7208  mkvprop  7233  nninfwlpoimlemg  7250  nninfwlpoimlemginf  7251  fzprval  10174  iseqf1olemnab  10610  iseqf1olemab  10611  iseqf1olemnanb  10612  iseqf1olemqk  10616  seq3f1olemqsumkj  10620  seq3f1olemqsumk  10621  seq3f1olemqsum  10622  fser0const  10644  expnnval  10651  expnegap0  10656  2zsupmax  11408  2zinfmin  11425  xrmaxifle  11428  xrmaxiflemab  11429  xrmaxiflemlub  11430  xrmaxiflemcom  11431  xrmaxrecl  11437  sumrbdclem  11559  summodclem3  11562  isumss  11573  isumss2  11575  fsumadd  11588  fsumsplit  11589  sumsplitdc  11614  fsummulc2  11630  cvgratz  11714  prodrbdclem  11753  prodmodclem2a  11758  fprodntrivap  11766  prod1dc  11768  fprodmul  11773  fprodsplitdc  11778  ef0lem  11842  gcdval  12151  nninfctlemfo  12232  eucalgf  12248  eucalginv  12249  eucalglt  12250  pcmpt  12537  pcmpt2  12538  ennnfonelemjn  12644  ennnfonelemp1  12648  ennnfonelemhdmp1  12651  ennnfonelemss  12652  ennnfonelemkh  12654  ennnfonelemhf1o  12655  unct  12684  fvprif  13045  gsumfzz  13197  gsumfzcl  13201  mulgnn  13332  mulgnegnn  13338  gsumfzreidx  13543  gsumfzsubmcl  13544  gsumfzmptfidmadd  13545  gsumfzmhm  13549  znf1o  14283  dvexp2  15032  elply2  15055  ply1termlem  15062  dvply1  15085  lgsval2lem  15335  lgsval4  15345  lgsval4a  15347  lgsneg  15349  lgsneg1  15350  lgsdilem  15352  lgsdir  15360  lgsne0  15363  gausslemma2dlem1a  15383  gausslemma2dlem1f1o  15385  gausslemma2dlem3  15388  2lgslem3  15426  bj-charfun  15537  bj-charfundc  15538  2omap  15726  nnsf  15736  peano4nninf  15737  nninfsellemsuc  15743  nninfsellemeq  15745  nninffeq  15751  dceqnconst  15791