| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > simplbi2 | Unicode version | ||
| Description: Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.) |
| Ref | Expression |
|---|---|
| pm3.26bi2.1 |
|
| Ref | Expression |
|---|---|
| simplbi2 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm3.26bi2.1 |
. . 3
| |
| 2 | 1 | biimpri 133 |
. 2
|
| 3 | 2 | ex 115 |
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 |
| This theorem depends on definitions: df-bi 117 |
| This theorem is referenced by: pm5.62dc 948 pm5.63dc 949 simplbi2com 1464 reuss2 3453 elni2 7427 elpq 9770 elfz0ubfz0 10247 elfzmlbp 10254 fzo1fzo0n0 10307 elfzo0z 10308 fzofzim 10312 elfzodifsumelfzo 10330 p1modz1 12105 dfgcd2 12335 algcvga 12373 pcprendvds 12613 |
| Copyright terms: Public domain | W3C validator |