Theorem iffalsed 3612

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 3610	. 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 1395   ifcif 3602

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 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-if 3603

This theorem is referenced by:  eqifdc  3639  ifnotdc  3641  ifandc  3643  mpodifsnif  6103  fimax2gtrilemstep  7071  updjudhcoinrg  7259  omp1eomlem  7272  difinfsnlem  7277  ctmlemr  7286  ctssdclemn0  7288  nnnninfeq  7306  nninfisol  7311  mkvprop  7336  nninfwlpoimlemg  7353  nninfwlpoimlemginf  7354  fzprval  10290  iseqf1olemnab  10735  iseqf1olemab  10736  iseqf1olemnanb  10737  iseqf1olemqk  10741  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  fser0const  10769  expnnval  10776  expnegap0  10781  ccatval2  11146  ccatalpha  11161  swrdnd  11207  swrd0g  11208  swrdccatin2  11277  2zsupmax  11753  2zinfmin  11770  xrmaxifle  11773  xrmaxiflemab  11774  xrmaxiflemlub  11775  xrmaxiflemcom  11776  xrmaxrecl  11782  sumrbdclem  11904  summodclem3  11907  isumss  11918  isumss2  11920  fsumadd  11933  fsumsplit  11934  sumsplitdc  11959  fsummulc2  11975  cvgratz  12059  prodrbdclem  12098  prodmodclem2a  12103  fprodntrivap  12111  prod1dc  12113  fprodmul  12118  fprodsplitdc  12123  ef0lem  12187  gcdval  12496  nninfctlemfo  12577  eucalgf  12593  eucalginv  12594  eucalglt  12595  pcmpt  12882  pcmpt2  12883  ennnfonelemjn  12989  ennnfonelemp1  12993  ennnfonelemhdmp1  12996  ennnfonelemss  12997  ennnfonelemkh  12999  ennnfonelemhf1o  13000  unct  13029  fvprif  13392  gsumfzz  13544  gsumfzcl  13548  mulgnn  13679  mulgnegnn  13685  gsumfzreidx  13890  gsumfzsubmcl  13891  gsumfzmptfidmadd  13892  gsumfzmhm  13896  znf1o  14631  dvexp2  15402  elply2  15425  ply1termlem  15432  dvply1  15455  lgsval2lem  15705  lgsval4  15715  lgsval4a  15717  lgsneg  15719  lgsneg1  15720  lgsdilem  15722  lgsdir  15730  lgsne0  15733  gausslemma2dlem1a  15753  gausslemma2dlem1f1o  15755  gausslemma2dlem3  15758  2lgslem3  15796  funvtxdm2domval  15846  funiedgdm2domval  15847  funvtxdm2vald  15848  funiedgdm2vald  15849  bj-charfun  16253  bj-charfundc  16254  2omap  16446  nnsf  16459  peano4nninf  16460  nninfsellemsuc  16466  nninfsellemeq  16468  nninffeq  16474  dceqnconst  16516