Theorem iffalsed 3589

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 3587	. 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 3579

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-if 3580

This theorem is referenced by:  eqifdc  3616  ifnotdc  3618  ifandc  3620  mpodifsnif  6061  fimax2gtrilemstep  7023  updjudhcoinrg  7209  omp1eomlem  7222  difinfsnlem  7227  ctmlemr  7236  ctssdclemn0  7238  nnnninfeq  7256  nninfisol  7261  mkvprop  7286  nninfwlpoimlemg  7303  nninfwlpoimlemginf  7304  fzprval  10239  iseqf1olemnab  10683  iseqf1olemab  10684  iseqf1olemnanb  10685  iseqf1olemqk  10689  seq3f1olemqsumkj  10693  seq3f1olemqsumk  10694  seq3f1olemqsum  10695  fser0const  10717  expnnval  10724  expnegap0  10729  ccatval2  11092  swrdnd  11150  swrd0g  11151  swrdccatin2  11220  2zsupmax  11652  2zinfmin  11669  xrmaxifle  11672  xrmaxiflemab  11673  xrmaxiflemlub  11674  xrmaxiflemcom  11675  xrmaxrecl  11681  sumrbdclem  11803  summodclem3  11806  isumss  11817  isumss2  11819  fsumadd  11832  fsumsplit  11833  sumsplitdc  11858  fsummulc2  11874  cvgratz  11958  prodrbdclem  11997  prodmodclem2a  12002  fprodntrivap  12010  prod1dc  12012  fprodmul  12017  fprodsplitdc  12022  ef0lem  12086  gcdval  12395  nninfctlemfo  12476  eucalgf  12492  eucalginv  12493  eucalglt  12494  pcmpt  12781  pcmpt2  12782  ennnfonelemjn  12888  ennnfonelemp1  12892  ennnfonelemhdmp1  12895  ennnfonelemss  12896  ennnfonelemkh  12898  ennnfonelemhf1o  12899  unct  12928  fvprif  13290  gsumfzz  13442  gsumfzcl  13446  mulgnn  13577  mulgnegnn  13583  gsumfzreidx  13788  gsumfzsubmcl  13789  gsumfzmptfidmadd  13790  gsumfzmhm  13794  znf1o  14528  dvexp2  15299  elply2  15322  ply1termlem  15329  dvply1  15352  lgsval2lem  15602  lgsval4  15612  lgsval4a  15614  lgsneg  15616  lgsneg1  15617  lgsdilem  15619  lgsdir  15627  lgsne0  15630  gausslemma2dlem1a  15650  gausslemma2dlem1f1o  15652  gausslemma2dlem3  15655  2lgslem3  15693  funvtxdm2domval  15743  funiedgdm2domval  15744  funvtxdm2vald  15745  funiedgdm2vald  15746  bj-charfun  15942  bj-charfundc  15943  2omap  16132  nnsf  16144  peano4nninf  16145  nninfsellemsuc  16151  nninfsellemeq  16153  nninffeq  16159  dceqnconst  16201