Theorem iffalse 3401

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		dedlemb 916	. . 3 |- ( -. ph -> ( x e. B <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
2	1	abbi2dv 2206	. 2 |- ( -. ph -> B = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
3		df-if 3394	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
4	2, 3	syl6reqr 2139	1 |- ( -. ph -> if ( ph , A , B ) = B )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 102   \/ wo 664   = wceq 1289   e. wcel 1438   {cab 2074   ifcif 3393

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-if 3394

This theorem is referenced by:  iffalsei  3402  iffalsed  3403  ifnefalse  3404  ifsbdc  3405  ifcldadc  3420  ifeq1dadc  3421  ifbothdadc  3422  ifbothdc  3423  ifiddc  3424  ifcldcd  3426  ifandc  3427  fidifsnen  6586  nnnninf  6806  uzin  9051  modifeq2int  9793  bcval  10157  bcval3  10159  isumrblem  10765  fisumcvg  10766  fsum3cvg  10767  isummolem2a  10771  sumsplitdc  10826  flodddiv4  11212  gcdn0val  11231  dfgcd2  11281  lcmn0val  11326