![]() |
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 1455 reuss2 3430 elni2 7331 elpq 9666 elfz0ubfz0 10143 elfzmlbp 10150 fzo1fzo0n0 10201 elfzo0z 10202 fzofzim 10206 elfzodifsumelfzo 10219 p1modz1 11819 dfgcd2 12033 algcvga 12069 pcprendvds 12308 |
Copyright terms: Public domain | W3C validator |