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 123 | . 2 |
4 | 1, 3 | bitri 173 | 1 |
Colors of variables: wff set class |
Syntax hints: 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: 3bitr2i 197 3bitr2ri 198 3bitr4i 201 3bitr4ri 202 imdistan 418 mpbiran 847 mpbiran2 848 3anrev 895 an6 1216 nfand 1460 19.33b2 1520 nf3 1559 nf4dc 1560 nf4r 1561 equsalh 1614 sb6x 1662 sb5f 1685 sbidm 1731 sb5 1767 sbanv 1769 sborv 1770 sbhb 1816 sb3an 1832 sbel2x 1874 sbal1yz 1877 sbexyz 1879 eu2 1944 2eu4 1993 cleqh 2137 cleqf 2201 dcne 2216 necon3bii 2243 ne3anior 2293 r2alf 2341 r2exf 2342 r19.23t 2423 r19.26-3 2443 r19.26m 2444 r19.43 2468 rabid2 2486 isset 2561 ralv 2571 rexv 2572 reuv 2573 rmov 2574 rexcom4b 2579 ceqsex4v 2597 ceqsex8v 2599 ceqsrexv 2674 ralrab2 2706 rexrab2 2708 reu2 2729 reu3 2731 reueq 2738 2reuswapdc 2743 reuind 2744 rmo2ilem 2847 dfss2 2934 dfss3 2935 dfss3f 2937 ssabral 3011 rabss 3017 ssrabeq 3026 uniiunlem 3028 uncom 3087 inass 3147 nsspssun 3170 indi 3184 difindiss 3191 difin2 3199 reupick3 3222 n0rf 3233 eq0 3239 eqv 3240 vss 3264 disj 3268 disj3 3272 undisj1 3279 undisj2 3280 exsnrex 3413 euabsn2 3439 euabsn 3440 prssg 3521 dfuni2 3582 unissb 3610 elint2 3622 ssint 3631 dfiin2g 3690 iunn0m 3717 iunxun 3735 iunxiun 3736 iinpw 3742 dftr2 3856 dftr5 3857 dftr3 3858 dftr4 3859 vprc 3888 inuni 3909 snelpw 3949 sspwb 3952 opelopabsb 3997 eusv2 4189 orddif 4271 onintexmid 4297 zfregfr 4298 tfi 4305 opthprc 4391 elxp3 4394 xpiundir 4399 elvv 4402 brinxp2 4407 relsn 4443 reliun 4458 inxp 4470 raliunxp 4477 rexiunxp 4478 cnvuni 4521 dm0rn0 4552 elrn 4577 ssdmres 4633 dfres2 4658 dfima2 4670 args 4694 cotr 4706 intasym 4709 asymref 4710 intirr 4711 cnv0 4727 xp11m 4759 cnvresima 4810 resco 4825 rnco 4827 coiun 4830 coass 4839 dfiota2 4868 dffun2 4912 dffun6f 4915 dffun4f 4918 dffun7 4928 dffun9 4930 funfn 4931 svrelfun 4964 imadiflem 4978 dffn2 5047 dffn3 5053 fintm 5075 dffn4 5112 dff1o4 5134 brprcneu 5171 eqfnfv3 5267 fnreseql 5277 fsn 5335 abrexco 5398 imaiun 5399 mpt22eqb 5610 elovmpt2 5701 abexex 5753 releldm2 5811 fnmpt2 5828 dftpos4 5878 tfrlem7 5933 0er 6140 eroveu 6197 erovlem 6198 domen 6232 reuen1 6281 ssfiexmid 6336 dmaddpq 6477 dmmulpq 6478 distrnqg 6485 enq0enq 6529 enq0tr 6532 nqnq0pi 6536 distrnq0 6557 prltlu 6585 prarloc 6601 genpdflem 6605 ltexprlemm 6698 ltexprlemlol 6700 ltexprlemupu 6702 ltexprlemdisj 6704 recexprlemdisj 6728 ltresr 6915 elnnz 8255 dfz2 8313 2rexuz 8525 eluz2b1 8539 elxr 8696 elixx1 8766 elioo2 8790 elioopnf 8836 elicopnf 8838 elfz1 8879 fzdifsuc 8943 fznn 8951 fzp1nel 8966 fznn0 8974 redivap 9474 imdivap 9481 climreu 9818 dcdc 9901 bj-vprc 10016 |
Copyright terms: Public domain | W3C validator |