Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > iftrue | Unicode version |
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.) |
Ref | Expression |
---|---|
iftrue |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dedlema 938 | . . 3 | |
2 | 1 | abbi2dv 2236 | . 2 |
3 | df-if 3445 | . 2 | |
4 | 2, 3 | syl6reqr 2169 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wa 103 wo 682 wceq 1316 wcel 1465 cab 2103 cif 3444 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in2 589 ax-io 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-11 1469 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-if 3445 |
This theorem is referenced by: iftruei 3450 iftrued 3451 ifsbdc 3456 ifcldadc 3471 ifbothdadc 3473 ifbothdc 3474 ifiddc 3475 ifcldcd 3477 ifandc 3478 fidifsnen 6732 nnnninf 6991 mkvprop 7000 uzin 9326 fzprval 9830 fztpval 9831 modifeq2int 10127 bcval 10463 bcval2 10464 sumrbdclem 11113 fsum3cvg 11114 summodclem2a 11118 isumss2 11130 fsum3ser 11134 fsumsplit 11144 sumsplitdc 11169 flodddiv4 11558 gcd0val 11576 dfgcd2 11629 eucalgf 11663 eucalginv 11664 eucalglt 11665 unct 11881 dvexp2 12772 nnsf 13126 nninfsellemsuc 13135 |
Copyright terms: Public domain | W3C validator |