Theorem iffalse 3630

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 3621	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
2		dedlemb 979	. . 3 |- ( -. ph -> ( x e. B <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
3	2	abbi2dv 2353	. 2 |- ( -. ph -> B = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
4	1, 3	eqtr4id 2284	1 |- ( -. ph -> if ( ph , A , B ) = B )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 716   = wceq 1398   e. wcel 2203   {cab 2218   ifcif 3620

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 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-if 3621

This theorem is referenced by:  iffalsei  3631  iffalsed  3632  ifnefalse  3633  ifsbdc  3635  ifcldadc  3652  ifeq1dadc  3653  ifeqdadc  3655  ifbothdadc  3656  ifbothdc  3657  ifiddc  3658  ifcldcd  3660  ifnotdc  3661  2if2dc  3662  ifandc  3663  ifordc  3664  ifnetruedc  3666  pw2f1odclem  7087  fidifsnen  7125  nnnninf  7417  uzin  9887  modifeq2int  10748  seqf1oglem1  10881  seqf1oglem2  10882  bcval  11111  bcval3  11113  swrdccat  11427  pfxccat3a  11430  swrdccat3b  11432  sumrbdclem  12063  fsum3cvg  12064  summodclem2a  12067  sumsplitdc  12118  prodrbdclem  12257  fproddccvg  12258  prodssdc  12275  flodddiv4  12622  gcdn0val  12657  dfgcd2  12710  lcmn0val  12763  pcgcd  13027  pcmptcl  13040  pcmpt  13041  pcmpt2  13042  pcprod  13044  fldivp1  13046  unct  13193  lgsneg  15897  lgsdilem  15900  lgsdir2  15906  lgsdir  15908  lgsdi  15910  lgsne0  15911  gausslemma2dlem1a  15931  2lgslem1c  15963  2lgs  15977