Theorem iffalsed 3484

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 3482	. 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 1331   ifcif 3474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-if 3475

This theorem is referenced by:  eqifdc  3506  ifandc  3508  mpodifsnif  5864  fimax2gtrilemstep  6794  updjudhcoinrg  6966  omp1eomlem  6979  difinfsnlem  6984  ctmlemr  6993  ctssdclemn0  6995  mkvprop  7032  fzprval  9869  iseqf1olemnab  10268  iseqf1olemab  10269  iseqf1olemnanb  10270  iseqf1olemqk  10274  seq3f1olemqsumkj  10278  seq3f1olemqsumk  10279  seq3f1olemqsum  10280  fser0const  10296  expnnval  10303  expnegap0  10308  2zsupmax  11004  xrmaxifle  11022  xrmaxiflemab  11023  xrmaxiflemlub  11024  xrmaxiflemcom  11025  xrmaxrecl  11031  sumrbdclem  11153  summodclem3  11156  isumss  11167  isumss2  11169  fsumadd  11182  fsumsplit  11183  sumsplitdc  11208  fsummulc2  11224  cvgratz  11308  prodrbdclem  11347  prodmodclem2a  11352  ef0lem  11373  gcdval  11655  eucalgf  11743  eucalginv  11744  eucalglt  11745  ennnfonelemjn  11922  ennnfonelemp1  11926  ennnfonelemhdmp1  11929  ennnfonelemss  11930  ennnfonelemkh  11932  ennnfonelemhf1o  11933  unct  11962  ressval2  12029  dvexp2  12855  nnsf  13209  peano4nninf  13210  nninfalllemn  13212  nninfsellemsuc  13218  nninfsellemeq  13220  nninffeq  13226