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 586 mpbiran 909 mpbiran2 910 3anrev 957 an6 1284 nfand 1532 19.33b2 1593 nf3 1632 nf4dc 1633 nf4r 1634 equsalh 1689 sb6x 1737 sb5f 1760 sbidm 1807 sb5 1843 sbanv 1845 sborv 1846 sbhb 1893 sb3an 1909 sbel2x 1951 sbal1yz 1954 sbexyz 1956 eu2 2021 2eu4 2070 cleqh 2217 cleqf 2282 dcne 2296 necon3bii 2323 ne3anior 2373 r2alf 2429 r2exf 2430 r19.23t 2516 r19.26-3 2539 r19.26m 2540 r19.43 2566 rabid2 2584 isset 2666 ralv 2677 rexv 2678 reuv 2679 rmov 2680 rexcom4b 2685 ceqsex4v 2703 ceqsex8v 2705 ceqsrexv 2789 ralrab2 2822 rexrab2 2824 reu2 2845 reu3 2847 reueq 2856 2reuswapdc 2861 reuind 2862 sbc3an 2942 rmo2ilem 2970 dfss2 3056 dfss3 3057 dfss3f 3059 ssabral 3138 rabss 3144 ssrabeq 3153 uniiunlem 3155 dfdif3 3156 ddifstab 3178 uncom 3190 inass 3256 indi 3293 difindiss 3300 difin2 3308 reupick3 3331 n0rf 3345 eq0 3351 eqv 3352 vss 3380 disj 3381 disj3 3385 undisj1 3390 undisj2 3391 exsnrex 3536 euabsn2 3562 euabsn 3563 prssg 3647 dfuni2 3708 unissb 3736 elint2 3748 ssint 3757 dfiin2g 3816 iunn0m 3843 iunxun 3862 iunxiun 3864 iinpw 3873 disjnim 3890 dftr2 3998 dftr5 3999 dftr3 4000 dftr4 4001 vnex 4029 inuni 4050 snelpw 4105 sspwb 4108 opelopabsb 4152 eusv2 4348 orddif 4432 onintexmid 4457 zfregfr 4458 tfi 4466 opthprc 4560 elxp3 4563 xpiundir 4568 elvv 4571 brinxp2 4576 relsn 4614 reliun 4630 inxp 4643 raliunxp 4650 rexiunxp 4651 cnvuni 4695 dm0rn0 4726 elrn 4752 ssdmres 4811 dfres2 4841 dfima2 4853 args 4878 cotr 4890 intasym 4893 asymref 4894 intirr 4895 cnv0 4912 xp11m 4947 cnvresima 4998 resco 5013 rnco 5015 coiun 5018 coass 5027 dfiota2 5059 dffun2 5103 dffun6f 5106 dffun4f 5109 dffun7 5120 dffun9 5122 funfn 5123 svrelfun 5158 imadiflem 5172 dffn2 5244 dffn3 5253 fintm 5278 dffn4 5321 dff1o4 5343 brprcneu 5382 eqfnfv3 5488 fnreseql 5498 fsn 5560 abrexco 5628 imaiun 5629 mpo2eqb 5848 elovmpo 5939 abexex 5992 releldm2 6051 fnmpo 6068 dftpos4 6128 tfrlem7 6182 0er 6431 eroveu 6488 erovlem 6489 map0e 6548 elixpconst 6568 domen 6613 reuen1 6663 xpf1o 6706 ssfilem 6737 finexdc 6764 ssfirab 6790 sbthlemi10 6822 djuexb 6897 dmaddpq 7155 dmmulpq 7156 distrnqg 7163 enq0enq 7207 enq0tr 7210 nqnq0pi 7214 distrnq0 7235 prltlu 7263 prarloc 7279 genpdflem 7283 ltexprlemm 7376 ltexprlemlol 7378 ltexprlemupu 7380 ltexprlemdisj 7382 recexprlemdisj 7406 ltresr 7615 elnnz 9022 dfz2 9081 2rexuz 9333 eluz2b1 9351 elxr 9518 elixx1 9635 elioo2 9659 elioopnf 9705 elicopnf 9707 elfz1 9750 fzdifsuc 9816 fznn 9824 fzp1nel 9839 fznn0 9848 redivap 10601 imdivap 10608 rexanre 10947 climreu 11021 3dvdsdec 11474 3dvds2dec 11475 bezoutlembi 11605 isprm2 11710 isprm3 11711 isprm4 11712 inffinp1 11853 isbasis3g 12124 restsn 12260 lmbr 12293 txbas 12338 tx2cn 12350 elcncf1di 12646 dedekindicclemicc 12690 limcrcl 12707 bj-nnor 12842 bj-vprc 12990 ss1oel2o 13085 subctctexmid 13092 |
Copyright terms: Public domain | W3C validator |