Theorem iffalsed 3615

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 3613	. 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 1397   ifcif 3605

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

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

This theorem is referenced by:  eqifdc  3642  ifnotdc  3644  ifandc  3646  mpodifsnif  6114  fimax2gtrilemstep  7090  updjudhcoinrg  7280  omp1eomlem  7293  difinfsnlem  7298  ctmlemr  7307  ctssdclemn0  7309  nnnninfeq  7327  nninfisol  7332  mkvprop  7357  nninfwlpoimlemg  7374  nninfwlpoimlemginf  7375  fzprval  10317  iseqf1olemnab  10764  iseqf1olemab  10765  iseqf1olemnanb  10766  iseqf1olemqk  10770  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  fser0const  10798  expnnval  10805  expnegap0  10810  ccatval2  11179  ccatalpha  11194  swrdnd  11244  swrd0g  11245  swrdccatin2  11314  2zsupmax  11804  2zinfmin  11821  xrmaxifle  11824  xrmaxiflemab  11825  xrmaxiflemlub  11826  xrmaxiflemcom  11827  xrmaxrecl  11833  sumrbdclem  11956  summodclem3  11959  isumss  11970  isumss2  11972  fsumadd  11985  fsumsplit  11986  sumsplitdc  12011  fsummulc2  12027  cvgratz  12111  prodrbdclem  12150  prodmodclem2a  12155  fprodntrivap  12163  prod1dc  12165  fprodmul  12170  fprodsplitdc  12175  ef0lem  12239  gcdval  12548  nninfctlemfo  12629  eucalgf  12645  eucalginv  12646  eucalglt  12647  pcmpt  12934  pcmpt2  12935  ennnfonelemjn  13041  ennnfonelemp1  13045  ennnfonelemhdmp1  13048  ennnfonelemss  13049  ennnfonelemkh  13051  ennnfonelemhf1o  13052  unct  13081  fvprif  13444  gsumfzz  13596  gsumfzcl  13600  mulgnn  13731  mulgnegnn  13737  gsumfzreidx  13942  gsumfzsubmcl  13943  gsumfzmptfidmadd  13944  gsumfzmhm  13948  znf1o  14684  dvexp2  15455  elply2  15478  ply1termlem  15485  dvply1  15508  lgsval2lem  15758  lgsval4  15768  lgsval4a  15770  lgsneg  15772  lgsneg1  15773  lgsdilem  15775  lgsdir  15783  lgsne0  15786  gausslemma2dlem1a  15806  gausslemma2dlem1f1o  15808  gausslemma2dlem3  15811  2lgslem3  15849  funvtxdm2domval  15899  funiedgdm2domval  15900  funvtxdm2vald  15901  funiedgdm2vald  15902  eupth2lem3lem4fi  16343  depindlem1  16376  bj-charfun  16453  bj-charfundc  16454  2omap  16645  nnsf  16658  peano4nninf  16659  nninfsellemsuc  16665  nninfsellemeq  16667  nninffeq  16673  dceqnconst  16716