Theorem iffalsed 3581

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 3579	. 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 1373   ifcif 3571

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-if 3572

This theorem is referenced by:  eqifdc  3607  ifnotdc  3609  ifandc  3610  mpodifsnif  6040  fimax2gtrilemstep  6999  updjudhcoinrg  7185  omp1eomlem  7198  difinfsnlem  7203  ctmlemr  7212  ctssdclemn0  7214  nnnninfeq  7232  nninfisol  7237  mkvprop  7262  nninfwlpoimlemg  7279  nninfwlpoimlemginf  7280  fzprval  10206  iseqf1olemnab  10648  iseqf1olemab  10649  iseqf1olemnanb  10650  iseqf1olemqk  10654  seq3f1olemqsumkj  10658  seq3f1olemqsumk  10659  seq3f1olemqsum  10660  fser0const  10682  expnnval  10689  expnegap0  10694  ccatval2  11057  swrdnd  11115  swrd0g  11116  2zsupmax  11570  2zinfmin  11587  xrmaxifle  11590  xrmaxiflemab  11591  xrmaxiflemlub  11592  xrmaxiflemcom  11593  xrmaxrecl  11599  sumrbdclem  11721  summodclem3  11724  isumss  11735  isumss2  11737  fsumadd  11750  fsumsplit  11751  sumsplitdc  11776  fsummulc2  11792  cvgratz  11876  prodrbdclem  11915  prodmodclem2a  11920  fprodntrivap  11928  prod1dc  11930  fprodmul  11935  fprodsplitdc  11940  ef0lem  12004  gcdval  12313  nninfctlemfo  12394  eucalgf  12410  eucalginv  12411  eucalglt  12412  pcmpt  12699  pcmpt2  12700  ennnfonelemjn  12806  ennnfonelemp1  12810  ennnfonelemhdmp1  12813  ennnfonelemss  12814  ennnfonelemkh  12816  ennnfonelemhf1o  12817  unct  12846  fvprif  13208  gsumfzz  13360  gsumfzcl  13364  mulgnn  13495  mulgnegnn  13501  gsumfzreidx  13706  gsumfzsubmcl  13707  gsumfzmptfidmadd  13708  gsumfzmhm  13712  znf1o  14446  dvexp2  15217  elply2  15240  ply1termlem  15247  dvply1  15270  lgsval2lem  15520  lgsval4  15530  lgsval4a  15532  lgsneg  15534  lgsneg1  15535  lgsdilem  15537  lgsdir  15545  lgsne0  15548  gausslemma2dlem1a  15568  gausslemma2dlem1f1o  15570  gausslemma2dlem3  15573  2lgslem3  15611  funvtxdm2domval  15659  funiedgdm2domval  15660  funvtxdm2vald  15661  funiedgdm2vald  15662  bj-charfun  15780  bj-charfundc  15781  2omap  15969  nnsf  15979  peano4nninf  15980  nninfsellemsuc  15986  nninfsellemeq  15988  nninffeq  15994  dceqnconst  16036