ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  iffalse Unicode version

Theorem iffalse 3381
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.
StepHypRef Expression
1 dedlemb 912 . . 3  |-  ( -. 
ph  ->  ( x  e.  B  <->  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) ) )
21abbi2dv 2201 . 2  |-  ( -. 
ph  ->  B  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) } )
3 df-if 3374 . 2  |-  if (
ph ,  A ,  B )  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) }
42, 3syl6reqr 2134 1  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 102    \/ wo 662    = wceq 1285    e. wcel 1434   {cab 2069   ifcif 3373
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 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-if 3374
This theorem is referenced by:  iffalsei  3382  iffalsed  3383  ifnefalse  3384  ifsbdc  3385  ifcldadc  3400  ifeq1dadc  3401  ifbothdadc  3402  ifbothdc  3403  ifcldcd  3405  fidifsnen  6516  nnnninf  8645  uzin  8946  modifeq2int  9682  expival  9794  bcval  9992  bcval3  9994  isumrblem  10573  fisumcvg  10574  flodddiv4  10714  gcdn0val  10733  dfgcd2  10783  lcmn0val  10828
  Copyright terms: Public domain W3C validator