![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bitr3d | Unicode version |
Description: Deduction form of bitr3i 175. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr3d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
bitr3d.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
bitr3d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr3d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | bicomd 129 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | bitr3d.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | bitrd 177 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 3bitrrd 204 3bitr3d 207 3bitr3rd 208 pm5.16 736 biassdc 1283 pm5.24dc 1286 anxordi 1288 sbequ12a 1653 drex1 1676 sbcomxyyz 1843 sb9v 1851 csbiebt 2880 prsspwg 3514 bnd2 3917 copsex2t 3973 copsex2g 3974 fnssresb 4954 fcnvres 5016 dmfco 5184 funimass5 5227 fmptco 5273 cbvfo 5368 cbvexfo 5369 isocnv 5394 isoini 5400 isoselem 5402 riota2df 5431 ovmpt2dxf 5568 caovcanrd 5606 ltpiord 6303 dfplpq2 6338 dfmpq2 6339 enqeceq 6343 enq0eceq 6420 enreceq 6664 cnegexlem3 6985 subeq0 7033 negcon1 7059 subeqrev 7170 lesub 7231 ltsub13 7233 subge0 7265 div11ap 7459 divmuleqap 7475 ltmuldiv2 7622 lemuldiv2 7629 nn1suc 7714 addltmul 7938 elnnnn0 8001 znn0sub 8085 prime 8113 indstr 8312 qapne 8350 fz1n 8678 fzrev3 8719 fzonlt0 8793 fzfig 8887 |
Copyright terms: Public domain | W3C validator |