| Intuitionistic Logic Explorer | 
      
      
      < Previous  
      Next >
      
       Nearby theorems  | 
  ||
| Mirrors > Home > ILE Home > Th. List > hbn | Unicode version | ||
| Description: If  | 
| Ref | Expression | 
|---|---|
| hbn.1 | 
 | 
| Ref | Expression | 
|---|---|
| hbn | 
 | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | hbnt 1667 | 
. 2
 | |
| 2 | hbn.1 | 
. 2
 | |
| 3 | 1, 2 | mpg 1465 | 
1
 | 
| Colors of variables: wff set class | 
| Syntax hints:    | 
| 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-in1 615 ax-in2 616 ax-5 1461 ax-gen 1463 ax-ie2 1508 ax-4 1524 ax-ial 1548 | 
| This theorem depends on definitions: df-bi 117 df-tru 1367 df-fal 1370 | 
| This theorem is referenced by: hbnae 1735 sbn 1971 euor 2071 euor2 2103 | 
| Copyright terms: Public domain | W3C validator |