Theorem iffalsed 3650

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 3648	. 2 |- ( -. ch -> if ( ch , A , B ) = B )
3	1, 2	syl 14	1 |- ( ph -> if ( ch , A , B ) = B )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   = wceq 1402   ifcif 3638

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-if 3639

This theorem is used by:  eqifdc  3677  ifnotdc  3679  ifandc  3681  ifeqeqxdc  3687  mpodifsnif  6184  fimax2gtrilemstep  7209  2omap  7324  updjudhcoinrg  7427  omp1eomlem  7440  difinfsnlem  7445  ctmlemr  7454  ctssdclemn0  7456  nnnninfeq  7474  nninfisol  7479  mkvprop  7504  nninfwlpoimlemg  7521  nninfwlpoimlemginf  7522  ind0  9310  fzprval  10506  iseqf1olemnab  10959  iseqf1olemab  10960  iseqf1olemnanb  10961  iseqf1olemqk  10965  seq3f1olemqsumkj  10969  seq3f1olemqsumk  10970  seq3f1olemqsum  10971  fser0const  10993  expnnval  11000  expnegap0  11005  ccatval2  11388  ccatalpha  11403  swrdnd  11453  swrd0g  11454  swrdccatin2  11523  2zsupmax  12015  2zinfmin  12034  xrmaxifle  12037  xrmaxiflemab  12038  xrmaxiflemlub  12039  xrmaxiflemcom  12040  xrmaxrecl  12046  sumrbdclem  12169  summodclem3  12172  isumss  12183  isumss2  12185  fsumadd  12198  fsumsplit  12199  sumsplitdc  12224  fsummulc2  12240  cvgratz  12324  prodrbdclem  12363  prodmodclem2a  12368  fprodntrivap  12376  prod1dc  12378  fprodmul  12383  fprodsplitdc  12388  ef0lem  12452  gcdval  12761  nninfctlemfo  12842  eucalgf  12858  eucalginv  12859  eucalglt  12860  pcmpt  13151  pcmpt2  13152  ballotfilemrv2  13323  ennnfonelemjn  13351  ennnfonelemp1  13355  ennnfonelemhdmp1  13358  ennnfonelemss  13359  ennnfonelemkh  13361  ennnfonelemhf1o  13362  unct  13391  fvprif  13723  gzsumcl  13863  mulgnn  13988  mulgnegnn  13994  gzsumreidx  14231  gzsumsubmcl  14232  gzsummhm  14235  znf1o  15095  psrlidmfi  15199  psrridmfi  15200  dvexp2  15935  elply2  15958  ply1termlem  15965  dvply1  15988  bposlem5  16312  lgsval2lem  16331  lgsval4  16341  lgsval4a  16343  lgsneg  16345  lgsneg1  16346  lgsdilem  16348  lgsdir  16356  lgsne0  16359  gausslemma2dlem1a  16379  gausslemma2dlem1f1o  16381  gausslemma2dlem3  16384  2lgslem3  16422  funvtxdm2domval  16472  funiedgdm2domval  16473  funvtxdm2vald  16474  funiedgdm2vald  16475  eupth2lem3lem4fi  16916  depindlem1  16949  bj-charfun  17035  bj-charfundc  17036  idjudju  17249  nnsf  17251  peano4nninf  17252  nninfsellemsuc  17258  nninfsellemeq  17260  nninffeq  17266  dceqnconst  17314