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 132 | . 2 |
3 | 2 | ex 114 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm5.62dc 940 pm5.63dc 941 simplbi2com 1437 reuss2 3407 elni2 7276 elpq 9607 elfz0ubfz0 10081 elfzmlbp 10088 fzo1fzo0n0 10139 elfzo0z 10140 fzofzim 10144 elfzodifsumelfzo 10157 p1modz1 11756 dfgcd2 11969 algcvga 12005 pcprendvds 12244 |
Copyright terms: Public domain | W3C validator |