![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bitr3d | Unicode version |
Description: Deduction form of bitr3i 186. (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 141 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | bitr3d.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | bitrd 188 |
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: 3bitrrd 215 3bitr3d 218 3bitr3rd 219 pm5.16 828 biassdc 1395 pm5.24dc 1398 anxordi 1400 sbequ12a 1773 drex1 1798 sbcomxyyz 1972 sb9v 1978 csbiebt 3096 prsspwg 3750 bnd2 4170 copsex2t 4242 copsex2g 4243 fnssresb 5324 fcnvres 5395 foelcdmi 5564 dmfco 5580 funimass5 5629 fmptco 5678 cbvfo 5780 cbvexfo 5781 isocnv 5806 isoini 5813 isoselem 5815 riota2df 5845 ovmpodxf 5994 caovcanrd 6032 fidcenumlemrks 6946 ordiso2 7028 ltpiord 7306 dfplpq2 7341 dfmpq2 7342 enqeceq 7346 enq0eceq 7424 enreceq 7723 ltpsrprg 7790 mappsrprg 7791 cnegexlem3 8121 subeq0 8170 negcon1 8196 subexsub 8316 subeqrev 8320 lesub 8385 ltsub13 8387 subge0 8419 div11ap 8643 divmuleqap 8660 ltmuldiv2 8818 lemuldiv2 8825 nn1suc 8924 addltmul 9141 elnnnn0 9205 znn0sub 9304 prime 9338 indstr 9579 qapne 9625 qlttri2 9627 fz1n 10027 fzrev3 10070 fzonlt0 10150 divfl0 10279 modqsubdir 10376 fzfig 10413 sqrt11 11029 sqrtsq2 11033 absdiflt 11082 absdifle 11083 nnabscl 11090 minclpr 11226 xrnegiso 11251 xrnegcon1d 11253 clim2 11272 climshft2 11295 sumrbdc 11368 prodrbdclem2 11562 fprodssdc 11579 sinbnd 11741 cosbnd 11742 dvdscmulr 11808 dvdsmulcr 11809 oddm1even 11860 qredeq 12076 cncongr2 12084 isprm3 12098 prmrp 12125 sqrt2irr 12142 crth 12204 pcdvdsb 12299 ssnnctlemct 12427 grpid 12799 grpidrcan 12821 grpidlcan 12822 grplmulf1o 12830 abladdsub4 12941 eltg3 13217 eltop 13229 eltop2 13230 eltop3 13231 lmbrf 13375 cncnpi 13388 txcn 13435 hmeoimaf1o 13474 ismet2 13514 xmseq0 13628 lgsne0 14099 2sqlem7 14117 |
Copyright terms: Public domain | W3C validator |