Theorem iffalse 3565

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 3558	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
2		dedlemb 972	. . 3 |- ( -. ph -> ( x e. B <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
3	2	abbi2dv 2312	. 2 |- ( -. ph -> B = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
4	1, 3	eqtr4id 2245	1 |- ( -. ph -> if ( ph , A , B ) = B )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 709   = wceq 1364   e. wcel 2164   {cab 2179   ifcif 3557

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 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-if 3558

This theorem is referenced by:  iffalsei  3566  iffalsed  3567  ifnefalse  3568  ifsbdc  3569  ifcldadc  3586  ifeq1dadc  3587  ifbothdadc  3589  ifbothdc  3590  ifiddc  3591  ifcldcd  3593  ifnotdc  3594  ifandc  3595  ifordc  3596  ifnetruedc  3598  pw2f1odclem  6890  fidifsnen  6926  nnnninf  7185  uzin  9625  modifeq2int  10457  seqf1oglem1  10590  seqf1oglem2  10591  bcval  10820  bcval3  10822  sumrbdclem  11520  fsum3cvg  11521  summodclem2a  11524  sumsplitdc  11575  prodrbdclem  11714  fproddccvg  11715  prodssdc  11732  flodddiv4  12075  gcdn0val  12098  dfgcd2  12151  lcmn0val  12204  pcgcd  12467  pcmptcl  12480  pcmpt  12481  pcmpt2  12482  pcprod  12484  fldivp1  12486  unct  12599  lgsneg  15140  lgsdilem  15143  lgsdir2  15149  lgsdir  15151  lgsdi  15153  lgsne0  15154  gausslemma2dlem1a  15174