Theorem iffalsed 3647

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 3645	. 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 1402   ifcif 3635

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 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 theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-if 3636

This theorem is referenced by:  eqifdc  3674  ifnotdc  3676  ifandc  3678  ifeqeqxdc  3684  mpodifsnif  6171  fimax2gtrilemstep  7195  2omap  7308  updjudhcoinrg  7411  omp1eomlem  7424  difinfsnlem  7429  ctmlemr  7438  ctssdclemn0  7440  nnnninfeq  7458  nninfisol  7463  mkvprop  7488  nninfwlpoimlemg  7505  nninfwlpoimlemginf  7506  fzprval  10467  iseqf1olemnab  10916  iseqf1olemab  10917  iseqf1olemnanb  10918  iseqf1olemqk  10922  seq3f1olemqsumkj  10926  seq3f1olemqsumk  10927  seq3f1olemqsum  10928  fser0const  10950  expnnval  10957  expnegap0  10962  ccatval2  11344  ccatalpha  11359  swrdnd  11409  swrd0g  11410  swrdccatin2  11479  2zsupmax  11970  2zinfmin  11987  xrmaxifle  11990  xrmaxiflemab  11991  xrmaxiflemlub  11992  xrmaxiflemcom  11993  xrmaxrecl  11999  sumrbdclem  12122  summodclem3  12125  isumss  12136  isumss2  12138  fsumadd  12151  fsumsplit  12152  sumsplitdc  12177  fsummulc2  12193  cvgratz  12277  prodrbdclem  12316  prodmodclem2a  12321  fprodntrivap  12329  prod1dc  12331  fprodmul  12336  fprodsplitdc  12341  ef0lem  12405  gcdval  12714  nninfctlemfo  12795  eucalgf  12811  eucalginv  12812  eucalglt  12813  pcmpt  13100  pcmpt2  13101  ballotfilemrv2  13243  ennnfonelemjn  13271  ennnfonelemp1  13275  ennnfonelemhdmp1  13278  ennnfonelemss  13279  ennnfonelemkh  13281  ennnfonelemhf1o  13282  unct  13311  fvprif  13641  gzsumcl  13781  mulgnn  13906  mulgnegnn  13912  gzsumreidx  14118  gzsumsubmcl  14119  gzsummhm  14122  znf1o  14958  dvexp2  15736  elply2  15759  ply1termlem  15766  dvply1  15789  lgsval2lem  16043  lgsval4  16053  lgsval4a  16055  lgsneg  16057  lgsneg1  16058  lgsdilem  16060  lgsdir  16068  lgsne0  16071  gausslemma2dlem1a  16091  gausslemma2dlem1f1o  16093  gausslemma2dlem3  16096  2lgslem3  16134  funvtxdm2domval  16184  funiedgdm2domval  16185  funvtxdm2vald  16186  funiedgdm2vald  16187  eupth2lem3lem4fi  16628  depindlem1  16661  bj-charfun  16747  bj-charfundc  16748  nnsf  16953  peano4nninf  16954  nninfsellemsuc  16960  nninfsellemeq  16962  nninffeq  16968  dceqnconst  17015