Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bitr4i | Unicode version |
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr4i.1 | |
bitr4i.2 |
Ref | Expression |
---|---|
bitr4i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr4i.1 | . 2 | |
2 | bitr4i.2 | . . 3 | |
3 | 2 | bicomi 131 | . 2 |
4 | 1, 3 | bitri 183 | 1 |
Colors of variables: wff set class |
Syntax hints: 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: 3bitr2i 207 3bitr2ri 208 3bitr4i 211 3bitr4ri 212 biancomi 268 imdistan 440 biadani 601 mpbiran 924 mpbiran2 925 3anrev 972 an6 1299 nfand 1547 19.33b2 1608 nf3 1647 nf4dc 1648 nf4r 1649 equsalh 1704 sb6x 1752 sb5f 1776 sbidm 1823 sb5 1859 sbanv 1861 sborv 1862 sbhb 1913 sb3an 1931 sbel2x 1973 sbal1yz 1976 sbexyz 1978 eu2 2043 2eu4 2092 cleqh 2239 cleqf 2305 dcne 2319 necon3bii 2346 ne3anior 2396 r2alf 2452 r2exf 2453 r19.23t 2539 r19.26-3 2562 r19.26m 2563 r19.43 2589 rabid2 2607 isset 2692 ralv 2703 rexv 2704 reuv 2705 rmov 2706 rexcom4b 2711 ceqsex4v 2729 ceqsex8v 2731 ceqsrexv 2815 ralrab2 2849 rexrab2 2851 reu2 2872 reu3 2874 reueq 2883 2reuswapdc 2888 reuind 2889 sbc3an 2970 rmo2ilem 2998 dfss2 3086 dfss3 3087 dfss3f 3089 ssabral 3168 rabss 3174 ssrabeq 3183 uniiunlem 3185 dfdif3 3186 ddifstab 3208 uncom 3220 inass 3286 indi 3323 difindiss 3330 difin2 3338 reupick3 3361 n0rf 3375 eq0 3381 eqv 3382 vss 3410 disj 3411 disj3 3415 undisj1 3420 undisj2 3421 exsnrex 3566 euabsn2 3592 euabsn 3593 prssg 3677 dfuni2 3738 unissb 3766 elint2 3778 ssint 3787 dfiin2g 3846 iunn0m 3873 iunxun 3892 iunxiun 3894 iinpw 3903 disjnim 3920 dftr2 4028 dftr5 4029 dftr3 4030 dftr4 4031 vnex 4059 inuni 4080 snelpw 4135 sspwb 4138 opelopabsb 4182 eusv2 4378 orddif 4462 onintexmid 4487 zfregfr 4488 tfi 4496 opthprc 4590 elxp3 4593 xpiundir 4598 elvv 4601 brinxp2 4606 relsn 4644 reliun 4660 inxp 4673 raliunxp 4680 rexiunxp 4681 cnvuni 4725 dm0rn0 4756 elrn 4782 ssdmres 4841 dfres2 4871 dfima2 4883 args 4908 cotr 4920 intasym 4923 asymref 4924 intirr 4925 cnv0 4942 xp11m 4977 cnvresima 5028 resco 5043 rnco 5045 coiun 5048 coass 5057 dfiota2 5089 dffun2 5133 dffun6f 5136 dffun4f 5139 dffun7 5150 dffun9 5152 funfn 5153 svrelfun 5188 imadiflem 5202 dffn2 5274 dffn3 5283 fintm 5308 dffn4 5351 dff1o4 5375 brprcneu 5414 eqfnfv3 5520 fnreseql 5530 fsn 5592 abrexco 5660 imaiun 5661 mpo2eqb 5880 elovmpo 5971 abexex 6024 releldm2 6083 fnmpo 6100 dftpos4 6160 tfrlem7 6214 0er 6463 eroveu 6520 erovlem 6521 map0e 6580 elixpconst 6600 domen 6645 reuen1 6695 xpf1o 6738 ssfilem 6769 finexdc 6796 ssfirab 6822 sbthlemi10 6854 djuexb 6929 dmaddpq 7187 dmmulpq 7188 distrnqg 7195 enq0enq 7239 enq0tr 7242 nqnq0pi 7246 distrnq0 7267 prltlu 7295 prarloc 7311 genpdflem 7315 ltexprlemm 7408 ltexprlemlol 7410 ltexprlemupu 7412 ltexprlemdisj 7414 recexprlemdisj 7438 ltresr 7647 elnnz 9064 dfz2 9123 2rexuz 9377 eluz2b1 9395 elxr 9563 elixx1 9680 elioo2 9704 elioopnf 9750 elicopnf 9752 elfz1 9795 fzdifsuc 9861 fznn 9869 fzp1nel 9884 fznn0 9893 redivap 10646 imdivap 10653 rexanre 10992 climreu 11066 prodmodc 11347 3dvdsdec 11562 3dvds2dec 11563 bezoutlembi 11693 isprm2 11798 isprm3 11799 isprm4 11800 inffinp1 11942 isbasis3g 12213 restsn 12349 lmbr 12382 txbas 12427 tx2cn 12439 elcncf1di 12735 dedekindicclemicc 12779 limcrcl 12796 bj-nnor 12946 bj-vprc 13094 ss1oel2o 13189 subctctexmid 13196 |
Copyright terms: Public domain | W3C validator |