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  7070  updjudhcoinrg  7256  omp1eomlem  7269  difinfsnlem  7274  ctmlemr  7283  ctssdclemn0  7285  nnnninfeq  7303  nninfisol  7308  mkvprop  7333  nninfwlpoimlemg  7350  nninfwlpoimlemginf  7351  fzprval  10286  iseqf1olemnab  10731  iseqf1olemab  10732  iseqf1olemnanb  10733  iseqf1olemqk  10737  seq3f1olemqsumkj  10741  seq3f1olemqsumk  10742  seq3f1olemqsum  10743  fser0const  10765  expnnval  10772  expnegap0  10777  ccatval2  11141  swrdnd  11199  swrd0g  11200  swrdccatin2  11269  2zsupmax  11745  2zinfmin  11762  xrmaxifle  11765  xrmaxiflemab  11766  xrmaxiflemlub  11767  xrmaxiflemcom  11768  xrmaxrecl  11774  sumrbdclem  11896  summodclem3  11899  isumss  11910  isumss2  11912  fsumadd  11925  fsumsplit  11926  sumsplitdc  11951  fsummulc2  11967  cvgratz  12051  prodrbdclem  12090  prodmodclem2a  12095  fprodntrivap  12103  prod1dc  12105  fprodmul  12110  fprodsplitdc  12115  ef0lem  12179  gcdval  12488  nninfctlemfo  12569  eucalgf  12585  eucalginv  12586  eucalglt  12587  pcmpt  12874  pcmpt2  12875  ennnfonelemjn  12981  ennnfonelemp1  12985  ennnfonelemhdmp1  12988  ennnfonelemss  12989  ennnfonelemkh  12991  ennnfonelemhf1o  12992  unct  13021  fvprif  13384  gsumfzz  13536  gsumfzcl  13540  mulgnn  13671  mulgnegnn  13677  gsumfzreidx  13882  gsumfzsubmcl  13883  gsumfzmptfidmadd  13884  gsumfzmhm  13888  znf1o  14623  dvexp2  15394  elply2  15417  ply1termlem  15424  dvply1  15447  lgsval2lem  15697  lgsval4  15707  lgsval4a  15709  lgsneg  15711  lgsneg1  15712  lgsdilem  15714  lgsdir  15722  lgsne0  15725  gausslemma2dlem1a  15745  gausslemma2dlem1f1o  15747  gausslemma2dlem3  15750  2lgslem3  15788  funvtxdm2domval  15838  funiedgdm2domval  15839  funvtxdm2vald  15840  funiedgdm2vald  15841  bj-charfun  16194  bj-charfundc  16195  2omap  16388  nnsf  16401  peano4nninf  16402  nninfsellemsuc  16408  nninfsellemeq  16410  nninffeq  16416  dceqnconst  16458