![]() |
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: ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 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 imdistan 434 mpbiran 887 mpbiran2 888 3anrev 935 an6 1258 nfand 1506 19.33b2 1566 nf3 1605 nf4dc 1606 nf4r 1607 equsalh 1662 sb6x 1710 sb5f 1733 sbidm 1780 sb5 1816 sbanv 1818 sborv 1819 sbhb 1865 sb3an 1881 sbel2x 1923 sbal1yz 1926 sbexyz 1928 eu2 1993 2eu4 2042 cleqh 2188 cleqf 2253 dcne 2267 necon3bii 2294 ne3anior 2344 r2alf 2396 r2exf 2397 r19.23t 2480 r19.26-3 2500 r19.26m 2501 r19.43 2526 rabid2 2544 isset 2626 ralv 2637 rexv 2638 reuv 2639 rmov 2640 rexcom4b 2645 ceqsex4v 2663 ceqsex8v 2665 ceqsrexv 2748 ralrab2 2781 rexrab2 2783 reu2 2804 reu3 2806 reueq 2815 2reuswapdc 2820 reuind 2821 sbc3an 2901 rmo2ilem 2929 dfss2 3015 dfss3 3016 dfss3f 3018 ssabral 3093 rabss 3099 ssrabeq 3108 uniiunlem 3110 dfdif3 3111 ddifstab 3133 uncom 3145 inass 3211 indi 3247 difindiss 3254 difin2 3262 reupick3 3285 n0rf 3299 eq0 3305 eqv 3306 vss 3334 disj 3335 disj3 3339 undisj1 3344 undisj2 3345 exsnrex 3489 euabsn2 3515 euabsn 3516 prssg 3600 dfuni2 3661 unissb 3689 elint2 3701 ssint 3710 dfiin2g 3769 iunn0m 3796 iunxun 3815 iunxiun 3816 iinpw 3825 disjnim 3842 dftr2 3944 dftr5 3945 dftr3 3946 dftr4 3947 vnex 3976 inuni 3997 snelpw 4049 sspwb 4052 opelopabsb 4096 eusv2 4292 orddif 4376 onintexmid 4401 zfregfr 4402 tfi 4410 opthprc 4502 elxp3 4505 xpiundir 4510 elvv 4513 brinxp2 4518 relsn 4556 reliun 4571 inxp 4583 raliunxp 4590 rexiunxp 4591 cnvuni 4635 dm0rn0 4666 elrn 4691 ssdmres 4748 dfres2 4777 dfima2 4789 args 4814 cotr 4826 intasym 4829 asymref 4830 intirr 4831 cnv0 4848 xp11m 4882 cnvresima 4933 resco 4948 rnco 4950 coiun 4953 coass 4962 dfiota2 4994 dffun2 5038 dffun6f 5041 dffun4f 5044 dffun7 5055 dffun9 5057 funfn 5058 svrelfun 5092 imadiflem 5106 dffn2 5176 dffn3 5184 fintm 5209 dffn4 5252 dff1o4 5274 brprcneu 5311 eqfnfv3 5413 fnreseql 5423 fsn 5483 abrexco 5552 imaiun 5553 mpt22eqb 5768 elovmpt2 5859 abexex 5911 releldm2 5969 fnmpt2 5986 dftpos4 6042 tfrlem7 6096 0er 6340 eroveu 6397 erovlem 6398 map0e 6457 elixpconst 6477 domen 6522 reuen1 6572 xpf1o 6614 ssfilem 6645 finexdc 6672 ssfirab 6697 sbthlemi10 6729 dmaddpq 6992 dmmulpq 6993 distrnqg 7000 enq0enq 7044 enq0tr 7047 nqnq0pi 7051 distrnq0 7072 prltlu 7100 prarloc 7116 genpdflem 7120 ltexprlemm 7213 ltexprlemlol 7215 ltexprlemupu 7217 ltexprlemdisj 7219 recexprlemdisj 7243 ltresr 7430 elnnz 8814 dfz2 8873 2rexuz 9124 eluz2b1 9142 elxr 9301 elixx1 9369 elioo2 9393 elioopnf 9439 elicopnf 9441 elfz1 9483 fzdifsuc 9549 fznn 9557 fzp1nel 9572 fznn0 9581 redivap 10362 imdivap 10369 rexanre 10707 climreu 10739 3dvdsdec 11197 3dvds2dec 11198 bezoutlembi 11326 isprm2 11431 isprm3 11432 isprm4 11433 isbasis3g 11798 elcncf1di 11901 dcdc 11928 bj-vprc 12053 ss1oel2o 12154 |
Copyright terms: Public domain | W3C validator |