![]() |
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 946 pm5.63dc 947 simplbi2com 1454 reuss2 3427 elni2 7326 elpq 9661 elfz0ubfz0 10138 elfzmlbp 10145 fzo1fzo0n0 10196 elfzo0z 10197 fzofzim 10201 elfzodifsumelfzo 10214 p1modz1 11814 dfgcd2 12028 algcvga 12064 pcprendvds 12303 |
Copyright terms: Public domain | W3C validator |