Theorem iffalsed 3571

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 3569	. 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 1364   ifcif 3561

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 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-if 3562

This theorem is referenced by:  eqifdc  3596  ifnotdc  3598  ifandc  3599  mpodifsnif  6015  fimax2gtrilemstep  6961  updjudhcoinrg  7147  omp1eomlem  7160  difinfsnlem  7165  ctmlemr  7174  ctssdclemn0  7176  nnnninfeq  7194  nninfisol  7199  mkvprop  7224  nninfwlpoimlemg  7241  nninfwlpoimlemginf  7242  fzprval  10157  iseqf1olemnab  10593  iseqf1olemab  10594  iseqf1olemnanb  10595  iseqf1olemqk  10599  seq3f1olemqsumkj  10603  seq3f1olemqsumk  10604  seq3f1olemqsum  10605  fser0const  10627  expnnval  10634  expnegap0  10639  2zsupmax  11391  2zinfmin  11408  xrmaxifle  11411  xrmaxiflemab  11412  xrmaxiflemlub  11413  xrmaxiflemcom  11414  xrmaxrecl  11420  sumrbdclem  11542  summodclem3  11545  isumss  11556  isumss2  11558  fsumadd  11571  fsumsplit  11572  sumsplitdc  11597  fsummulc2  11613  cvgratz  11697  prodrbdclem  11736  prodmodclem2a  11741  fprodntrivap  11749  prod1dc  11751  fprodmul  11756  fprodsplitdc  11761  ef0lem  11825  gcdval  12126  nninfctlemfo  12207  eucalgf  12223  eucalginv  12224  eucalglt  12225  pcmpt  12512  pcmpt2  12513  ennnfonelemjn  12619  ennnfonelemp1  12623  ennnfonelemhdmp1  12626  ennnfonelemss  12627  ennnfonelemkh  12629  ennnfonelemhf1o  12630  unct  12659  fvprif  12986  gsumfzz  13127  gsumfzcl  13131  mulgnn  13256  mulgnegnn  13262  gsumfzreidx  13467  gsumfzsubmcl  13468  gsumfzmptfidmadd  13469  gsumfzmhm  13473  znf1o  14207  dvexp2  14948  elply2  14971  ply1termlem  14978  dvply1  15001  lgsval2lem  15251  lgsval4  15261  lgsval4a  15263  lgsneg  15265  lgsneg1  15266  lgsdilem  15268  lgsdir  15276  lgsne0  15279  gausslemma2dlem1a  15299  gausslemma2dlem1f1o  15301  gausslemma2dlem3  15304  2lgslem3  15342  bj-charfun  15453  bj-charfundc  15454  nnsf  15649  peano4nninf  15650  nninfsellemsuc  15656  nninfsellemeq  15658  nninffeq  15664  dceqnconst  15704