| 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 947 pm5.63dc 948 simplbi2com 1463 reuss2 3452 elni2 7426 elpq 9769 elfz0ubfz0 10246 elfzmlbp 10253 fzo1fzo0n0 10305 elfzo0z 10306 fzofzim 10310 elfzodifsumelfzo 10328 p1modz1 12076 dfgcd2 12306 algcvga 12344 pcprendvds 12584 |
| Copyright terms: Public domain | W3C validator |