Theorem iffalse 3544

Description: Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.)

Assertion

Ref	Expression
iffalse	|- ( -. ph -> if ( ph , A , B ) = B )

Proof of Theorem iffalse

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-if 3537	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
2		dedlemb 970	. . 3 |- ( -. ph -> ( x e. B <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
3	2	abbi2dv 2296	. 2 |- ( -. ph -> B = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
4	1, 3	eqtr4id 2229	1 |- ( -. ph -> if ( ph , A , B ) = B )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 708   = wceq 1353   e. wcel 2148   {cab 2163   ifcif 3536

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 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-if 3537

This theorem is referenced by:  iffalsei  3545  iffalsed  3546  ifnefalse  3547  ifsbdc  3548  ifcldadc  3565  ifeq1dadc  3566  ifbothdadc  3568  ifbothdc  3569  ifiddc  3570  ifcldcd  3572  ifnotdc  3573  ifandc  3574  ifordc  3575  fidifsnen  6873  nnnninf  7127  uzin  9563  modifeq2int  10389  bcval  10732  bcval3  10734  sumrbdclem  11388  fsum3cvg  11389  summodclem2a  11392  sumsplitdc  11443  prodrbdclem  11582  fproddccvg  11583  prodssdc  11600  flodddiv4  11942  gcdn0val  11965  dfgcd2  12018  lcmn0val  12069  pcgcd  12331  pcmptcl  12343  pcmpt  12344  pcmpt2  12345  pcprod  12347  fldivp1  12349  unct  12446  lgsneg  14586  lgsdilem  14589  lgsdir2  14595  lgsdir  14597  lgsdi  14599  lgsne0  14600