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

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.
StepHypRef Expression
1 dedlemb 916 . . 3  |-  ( -. 
ph  ->  ( x  e.  B  <->  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) ) )
21abbi2dv 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 ) ) }
42, 3syl6reqr 2139 1  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator