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

Theorem iftrue 3374
Description: Value of the conditional operator when its first argument is true. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
iftrue  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )

Proof of Theorem iftrue
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dedlema 911 . . 3  |-  ( ph  ->  ( x  e.  A  <->  ( ( x  e.  A  /\  ph )  \/  (
x  e.  B  /\  -.  ph ) ) ) )
21abbi2dv 2201 . 2  |-  ( ph  ->  A  =  { x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) } )
3 df-if 3370 . 2  |-  if (
ph ,  A ,  B )  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) }
42, 3syl6reqr 2134 1  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 102    \/ wo 662    = wceq 1285    e. wcel 1434   {cab 2069   ifcif 3369
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 3370
This theorem is referenced by:  iftruei  3375  iftrued  3376  ifsbdc  3381  ifcldadc  3396  ifbothdadc  3398  ifbothdc  3399  ifcldcd  3400  fidifsnen  6428  uzin  8809  fzprval  9252  fztpval  9253  modifeq2int  9545  expival  9652  bcval  9850  bcval2  9851  isumrblem  10425  fisumcvg  10426  flodddiv4  10566  gcd0val  10584  dfgcd2  10635  eucalgf  10669  eucalginv  10670  eucalglt  10671
  Copyright terms: Public domain W3C validator