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: wi 4 wb 98 |
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 737 biassdc 1286 pm5.24dc 1289 anxordi 1291 sbequ12a 1656 drex1 1679 sbcomxyyz 1846 sb9v 1854 csbiebt 2886 prsspwg 3523 bnd2 3926 copsex2t 3982 copsex2g 3983 fnssresb 5011 fcnvres 5073 dmfco 5241 funimass5 5284 fmptco 5330 cbvfo 5425 cbvexfo 5426 isocnv 5451 isoini 5457 isoselem 5459 riota2df 5488 ovmpt2dxf 5626 caovcanrd 5664 ordiso2 6357 ltpiord 6417 dfplpq2 6452 dfmpq2 6453 enqeceq 6457 enq0eceq 6535 enreceq 6821 cnegexlem3 7188 subeq0 7237 negcon1 7263 subeqrev 7374 lesub 7436 ltsub13 7438 subge0 7470 div11ap 7677 divmuleqap 7693 ltmuldiv2 7841 lemuldiv2 7848 nn1suc 7933 addltmul 8161 elnnnn0 8225 znn0sub 8309 prime 8337 indstr 8536 qapne 8574 fz1n 8908 fzrev3 8949 fzonlt0 9023 divfl0 9138 fzfig 9206 sqrt11 9637 sqrtsq2 9641 absdiflt 9688 absdifle 9689 nnabscl 9696 clim2 9804 climshft2 9827 sqrt2irr 9878 |
Copyright terms: Public domain | W3C validator |