Theorem iffalsed 3619

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 3617	. 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 1398   ifcif 3607

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 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-if 3608

This theorem is referenced by:  eqifdc  3646  ifnotdc  3648  ifandc  3650  mpodifsnif  6124  fimax2gtrilemstep  7133  updjudhcoinrg  7340  omp1eomlem  7353  difinfsnlem  7358  ctmlemr  7367  ctssdclemn0  7369  nnnninfeq  7387  nninfisol  7392  mkvprop  7417  nninfwlpoimlemg  7434  nninfwlpoimlemginf  7435  fzprval  10379  iseqf1olemnab  10826  iseqf1olemab  10827  iseqf1olemnanb  10828  iseqf1olemqk  10832  seq3f1olemqsumkj  10836  seq3f1olemqsumk  10837  seq3f1olemqsum  10838  fser0const  10860  expnnval  10867  expnegap0  10872  ccatval2  11241  ccatalpha  11256  swrdnd  11306  swrd0g  11307  swrdccatin2  11376  2zsupmax  11866  2zinfmin  11883  xrmaxifle  11886  xrmaxiflemab  11887  xrmaxiflemlub  11888  xrmaxiflemcom  11889  xrmaxrecl  11895  sumrbdclem  12018  summodclem3  12021  isumss  12032  isumss2  12034  fsumadd  12047  fsumsplit  12048  sumsplitdc  12073  fsummulc2  12089  cvgratz  12173  prodrbdclem  12212  prodmodclem2a  12217  fprodntrivap  12225  prod1dc  12227  fprodmul  12232  fprodsplitdc  12237  ef0lem  12301  gcdval  12610  nninfctlemfo  12691  eucalgf  12707  eucalginv  12708  eucalglt  12709  pcmpt  12996  pcmpt2  12997  ennnfonelemjn  13103  ennnfonelemp1  13107  ennnfonelemhdmp1  13110  ennnfonelemss  13111  ennnfonelemkh  13113  ennnfonelemhf1o  13114  unct  13143  fvprif  13506  gsumfzz  13658  gsumfzcl  13662  mulgnn  13793  mulgnegnn  13799  gsumfzreidx  14004  gsumfzsubmcl  14005  gsumfzmptfidmadd  14006  gsumfzmhm  14010  znf1o  14747  dvexp2  15523  elply2  15546  ply1termlem  15553  dvply1  15576  lgsval2lem  15829  lgsval4  15839  lgsval4a  15841  lgsneg  15843  lgsneg1  15844  lgsdilem  15846  lgsdir  15854  lgsne0  15857  gausslemma2dlem1a  15877  gausslemma2dlem1f1o  15879  gausslemma2dlem3  15882  2lgslem3  15920  funvtxdm2domval  15970  funiedgdm2domval  15971  funvtxdm2vald  15972  funiedgdm2vald  15973  eupth2lem3lem4fi  16414  depindlem1  16447  bj-charfun  16523  bj-charfundc  16524  2omap  16715  nnsf  16731  peano4nninf  16732  nninfsellemsuc  16738  nninfsellemeq  16740  nninffeq  16746  dceqnconst  16793