![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bitr3i | Unicode version |
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr3i.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
bitr3i.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
bitr3i |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr3i.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | bicomi 132 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | bitr3i.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | bitri 184 |
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: 3bitrri 207 3bitr3i 210 3bitr3ri 211 anandi 590 anandir 591 xchnxbi 680 orordi 773 orordir 774 sbco3v 1969 sbco4 2007 elsb1 2155 elsb2 2156 abeq1i 2289 cbvabw 2300 r19.41 2632 rexcom4a 2761 moeq 2912 mosubt 2914 2reuswapdc 2941 nfcdeq 2959 sbcid 2978 sbcco2 2985 sbc7 2989 sbcie2g 2996 eqsbc1 3002 sbcralt 3039 sbcrext 3040 cbvralcsf 3119 cbvrexcsf 3120 cbvrabcsf 3122 abss 3224 ssab 3225 difrab 3409 abn0m 3448 prsspw 3763 disjnim 3991 brab1 4047 unopab 4079 exss 4223 uniuni 4447 elvvv 4685 eliunxp 4761 ralxp 4765 rexxp 4766 opelco 4794 reldm0 4840 resieq 4912 resiexg 4947 iss 4948 imai 4979 cnvsym 5007 intasym 5008 asymref 5009 codir 5012 poirr2 5016 rninxp 5067 cnvsom 5167 funopg 5245 fin 5397 f1cnvcnv 5427 fndmin 5618 resoprab 5964 mpo2eqb 5977 ov6g 6005 offval 6083 dfopab2 6183 dfoprab3s 6184 fmpox 6194 spc2ed 6227 brtpos0 6246 dftpos3 6256 tpostpos 6258 ercnv 6549 xpcomco 6819 xpassen 6823 phpm 6858 ctssdccl 7103 elni2 7291 elfz2nn0 10085 elfzmlbp 10105 clim0 11264 nnwosdc 12010 isstructim 12446 srgrmhm 12990 ntreq0 13265 cnmptcom 13431 dedekindicclemicc 13743 |
Copyright terms: Public domain | W3C validator |