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  6181  fimax2gtrilemstep  7205  2omap  7318  updjudhcoinrg  7421  omp1eomlem  7434  difinfsnlem  7439  ctmlemr  7448  ctssdclemn0  7450  nnnninfeq  7468  nninfisol  7473  mkvprop  7498  nninfwlpoimlemg  7515  nninfwlpoimlemginf  7516  ind0  9301  fzprval  10489  iseqf1olemnab  10938  iseqf1olemab  10939  iseqf1olemnanb  10940  iseqf1olemqk  10944  seq3f1olemqsumkj  10948  seq3f1olemqsumk  10949  seq3f1olemqsum  10950  fser0const  10972  expnnval  10979  expnegap0  10984  ccatval2  11366  ccatalpha  11381  swrdnd  11431  swrd0g  11432  swrdccatin2  11501  2zsupmax  11992  2zinfmin  12009  xrmaxifle  12012  xrmaxiflemab  12013  xrmaxiflemlub  12014  xrmaxiflemcom  12015  xrmaxrecl  12021  sumrbdclem  12144  summodclem3  12147  isumss  12158  isumss2  12160  fsumadd  12173  fsumsplit  12174  sumsplitdc  12199  fsummulc2  12215  cvgratz  12299  prodrbdclem  12338  prodmodclem2a  12343  fprodntrivap  12351  prod1dc  12353  fprodmul  12358  fprodsplitdc  12363  ef0lem  12427  gcdval  12736  nninfctlemfo  12817  eucalgf  12833  eucalginv  12834  eucalglt  12835  pcmpt  13122  pcmpt2  13123  ballotfilemrv2  13265  ennnfonelemjn  13293  ennnfonelemp1  13297  ennnfonelemhdmp1  13300  ennnfonelemss  13301  ennnfonelemkh  13303  ennnfonelemhf1o  13304  unct  13333  fvprif  13664  gzsumcl  13804  mulgnn  13929  mulgnegnn  13935  gzsumreidx  14141  gzsumsubmcl  14142  gzsummhm  14145  znf1o  14986  dvexp2  15813  elply2  15836  ply1termlem  15843  dvply1  15866  lgsval2lem  16129  lgsval4  16139  lgsval4a  16141  lgsneg  16143  lgsneg1  16144  lgsdilem  16146  lgsdir  16154  lgsne0  16157  gausslemma2dlem1a  16177  gausslemma2dlem1f1o  16179  gausslemma2dlem3  16182  2lgslem3  16220  funvtxdm2domval  16270  funiedgdm2domval  16271  funvtxdm2vald  16272  funiedgdm2vald  16273  eupth2lem3lem4fi  16714  depindlem1  16747  bj-charfun  16833  bj-charfundc  16834  nnsf  17048  peano4nninf  17049  nninfsellemsuc  17055  nninfsellemeq  17057  nninffeq  17063  dceqnconst  17110