Theorem iffalsed 4097

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 4095	. 2 |- ( -. ch -> if ( ch , A , B ) = B )
3	1, 2	syl 17	1 |- ( ph -> if ( ch , A , B ) = B )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1483   ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  ifeqor  4132  ifnot  4133  ifan  4134  somincom  5530  mpt2difsnif  6753  tz7.44-2  7503  tz7.44-3  7504  unxpdomlem2  8165  sniffsupp  8315  unwdomg  8489  cantnfp1lem1  8575  cantnfp1lem3  8577  cantnflem1d  8585  ttukeylem7  9337  canthp1lem2  9475  pwfseqlem3  9482  xmulneg1  12099  rexmul  12101  xmulpnf1  12104  fzprval  12401  expnnval  12863  expneg  12868  ccatval2  13362  ccatalpha  13375  swrdnd  13432  swrdnd2  13433  swrd0  13434  swrdccatin2  13487  relexpsucnnr  13765  relexp1g  13766  sgnp  13830  sgnn  13834  absmax  14069  sumss2  14457  fsumsplit  14471  fprodntriv  14672  fprodsplit  14696  ef0lem  14809  rpnnen2lem9  14951  sadadd2  15182  eucalgf  15296  eucalginv  15297  eucalglt  15298  iserodd  15540  pcmpt  15596  pcmpt2  15597  ramtub  15716  gsumval2a  17279  mgm2nsgrplem2  17406  mgm2nsgrplem3  17407  sgrp2nmndlem3  17412  mulgnn  17547  mulgnegnn  17551  symgextfv  17838  pmtrprfv3  17874  pmtrdifellem4  17899  pmtrprfval  17907  pmtrprfvalrn  17908  odlem2  17958  dfod2  17981  gsumval3a  18304  gsumzsplit  18327  dmdprdsplitlem  18436  abvtrivd  18840  psrlidm  19403  psrridm  19404  mvrcl  19449  mplmon  19463  mplmonmul  19464  mplcoe1  19465  mplcoe5  19468  evlslem3  19514  coe1tmfv2  19645  cply1coe0  19669  cply1coe0bi  19670  gsummoncoe1  19674  uvcvv0  20129  uvcff  20130  mulmarep1gsum1  20379  1marepvsma1  20389  mdetunilem2  20419  mdetunilem9  20426  maducoeval2  20446  symgmatr01lem  20459  gsummatr01lem3  20463  gsummatr01lem4  20464  gsummatr01  20465  m2cpm  20546  m2cpminvid2lem  20559  pmatcollpw3fi1lem1  20591  mp2pm2mplem4  20614  chfacffsupp  20661  chfacfscmul0  20663  chfacfpmmul0  20667  ptpjpre2  21383  ptopn2  21387  xkopt  21458  tsmssplit  21955  xrsxmet  22612  htpycc  22779  pco1  22815  pcohtpylem  22819  pcoass  22824  pcorevlem  22826  ovolunlem1a  23264  ovolunlem1  23265  ovolicc1  23284  itg11  23458  mbfi1flim  23490  itg2split  23516  itg2cnlem1  23528  itgeq2  23544  itgss2  23579  itgss3  23581  itgless  23583  ibladdlem  23586  itgaddlem1  23589  itggt0  23608  itgcn  23609  dvexp2  23717  lhop2  23778  deg1add  23863  ig1pval3  23934  ply1termlem  23959  plyeq0lem  23966  plypf1  23968  dvply1  24039  pserdvlem2  24182  abelthlem9  24194  logtayllem  24405  logtayl  24406  cxpef  24411  rlimcnp2  24693  efrlim  24696  muinv  24919  bposlem5  25013  lgsval2lem  25032  lgsval4  25042  lgsval4a  25044  lgsneg  25046  lgsneg1  25047  lgsdilem  25049  lgsdir  25057  lgsne0  25060  gausslemma2dlem1a  25090  gausslemma2dlem3  25093  2lgslem3  25129  rplogsumlem2  25174  dchrisum0fno1  25200  rplogsum  25216  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  padicabv  25319  ostth1  25322  ostth3  25327  axlowdim  25841  vtxval  25878  iedgval  25879  funvtxdmge2val  25891  funiedgdmge2val  25892  funvtxdm2val  25893  funiedgdm2val  25894  funvtxdm2valOLD  25895  funiedgdm2valOLD  25896  funvtxdmge2valOLD  25899  funiedgdmge2valOLD  25900  snstrvtxval  25929  snstriedgval  25930  crctcshwlkn0lem3  26704  crctcsh  26716  clwlkclwwlklem2fv2  26897  eucrct2eupth  27105  partfun  29475  psgnfzto1stlem  29850  pmtridfv1  29857  pmtridfv2  29858  smattr  29865  smatbl  29866  smatbr  29867  1smat1  29870  submatminr1  29876  madjusmdetlem1  29893  madjusmdetlem2  29894  xrge0iifcv  29980  xrge0iif1  29984  ind0  30080  esumpinfval  30135  sigaclfu2  30184  eulerpartlemgs2  30442  ballotlemrv2  30583  signswmnd  30634  signswlid  30636  signsvtp  30660  signlem0  30664  mrsubcn  31416  bcneg1  31622  bccolsum  31625  dfrdg2  31701  dfrdg4  32058  unblimceq0lem  32497  unbdqndv2lem2  32501  finxpreclem3  33230  finxpreclem5  33232  poimirlem1  33410  poimirlem2  33411  poimirlem7  33416  poimirlem10  33419  poimirlem11  33420  poimirlem16  33425  poimirlem17  33426  poimirlem20  33429  poimirlem24  33433  mblfinlem2  33447  itg2addnclem2  33462  ibladdnclem  33466  ftc1anclem6  33490  ftc1anclem8  33492  fdc  33541  heiborlem6  33615  cdleme31fv2  35681  cdlemefr27cl  35691  kelac1  37633  flcidc  37744  relexp01min  38005  relexpxpmin  38009  clsk1indlem0  38339  refsum2cnlem1  39196  upbdrech2  39522  ssfiunibd  39523  ioondisj2  39714  limsup10exlem  40004  icccncfext  40100  cncfiooicclem1  40106  cncfioobdlem  40109  dvnxpaek  40157  dvnprodlem1  40161  ditgeqiooicc  40176  iblcncfioo  40194  volioore  40207  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem40  40364  fourierdlem56  40379  fourierdlem65  40388  fourierdlem66  40389  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem78  40401  fourierdlem79  40402  fourierdlem81  40404  fourierdlem82  40405  fourierdlem97  40420  fourierdlem103  40426  fourierdlem104  40427  sqwvfoura  40445  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  etransclem4  40455  etransclem14  40465  etransclem20  40471  etransclem22  40473  etransclem24  40475  etransclem25  40476  etransclem31  40482  etransclem32  40483  etransclem35  40486  sge0reval  40589  sge0sn  40596  nnfoctbdjlem  40672  isomenndlem  40744  ovnn0val  40765  ovnsubaddlem1  40784  hoidmvn0val  40798  hsphoidmvle2  40799  hsphoidmvle  40800  hoidmvval0  40801  hoidmv1lelem2  40806  hoidmvlelem2  40810  hoidmvlelem3  40811  ovnhoilem1  40815  hspmbllem1  40840  hspmbllem2  40841  volico2  40855  ovolval2lem  40857  ovnsubadd2lem  40859  ovolval4lem1  40863  ovnovollem3  40872  vonioo  40896  vonicc  40899  fdmdifeqresdif  42120  dig1  42402  dignn0flhalflem1  42409