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  15938  elply2  15961  ply1termlem  15968  dvply1  15991  bposlem5  16315  lgsval2lem  16334  lgsval4  16344  lgsval4a  16346  lgsneg  16348  lgsneg1  16349  lgsdilem  16351  lgsdir  16359  lgsne0  16362  gausslemma2dlem1a  16382  gausslemma2dlem1f1o  16384  gausslemma2dlem3  16387  2lgslem3  16425  funvtxdm2domval  16475  funiedgdm2domval  16476  funvtxdm2vald  16477  funiedgdm2vald  16478  eupth2lem3lem4fi  16919  depindlem1  16952  bj-charfun  17038  bj-charfundc  17039  idjudju  17252  nnsf  17254  peano4nninf  17255  nninfsellemsuc  17261  nninfsellemeq  17263  nninffeq  17269  dceqnconst  17317