![]() |
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 132 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 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: 3bitr2i 208 3bitr2ri 209 3bitr4i 212 3bitr4ri 213 biancomi 270 imdistan 444 bianass 469 biadani 612 mpbiran 940 mpbiran2 941 3anrev 988 an6 1321 nfand 1568 19.33b2 1629 nf3 1669 nf4dc 1670 nf4r 1671 equsalh 1726 sb6x 1779 sb5f 1804 sbidm 1851 sb5 1887 sbanv 1889 sborv 1890 sbhb 1940 sb3an 1958 sbel2x 1998 sbal1yz 2001 sbexyz 2003 eu2 2070 2eu4 2119 cleqh 2277 cleqf 2344 dcne 2358 necon3bii 2385 ne3anior 2435 r2alf 2494 r2exf 2495 r19.23t 2584 r19.26-3 2607 r19.26m 2608 r19.43 2635 rabid2 2654 isset 2745 ralv 2756 rexv 2757 reuv 2758 rmov 2759 rexcom4b 2764 ceqsex4v 2782 ceqsex8v 2784 ceqsrexv 2869 ralrab2 2904 rexrab2 2906 reu2 2927 reu3 2929 reueq 2938 2reuswapdc 2943 reuind 2944 sbc3an 3026 rmo2ilem 3054 csbcow 3070 dfss2 3146 dfss3 3147 dfss3f 3149 ssabral 3228 rabss 3234 ssrabeq 3244 uniiunlem 3246 dfdif3 3247 ddifstab 3269 uncom 3281 inass 3347 indi 3384 difindiss 3391 difin2 3399 reupick3 3422 n0rf 3437 eq0 3443 eqv 3444 vss 3472 disj 3473 disj3 3477 undisj1 3482 undisj2 3483 exsnrex 3636 euabsn2 3663 euabsn 3664 prssg 3751 dfuni2 3813 unissb 3841 elint2 3853 ssint 3862 dfiin2g 3921 iunn0m 3949 iunxun 3968 iunxiun 3970 iinpw 3979 disjnim 3996 dftr2 4105 dftr5 4106 dftr3 4107 dftr4 4108 vnex 4136 inuni 4157 snelpw 4215 sspwb 4218 opelopabsb 4262 eusv2 4459 orddif 4548 onintexmid 4574 zfregfr 4575 tfi 4583 opthprc 4679 elxp3 4682 xpiundir 4687 elvv 4690 brinxp2 4695 relsn 4733 reliun 4749 inxp 4763 raliunxp 4770 rexiunxp 4771 cnvuni 4815 dm0rn0 4846 elrn 4872 ssdmres 4931 dfres2 4961 dfima2 4974 args 4999 cotr 5012 intasym 5015 asymref 5016 intirr 5017 cnv0 5034 xp11m 5069 cnvresima 5120 resco 5135 rnco 5137 coiun 5140 coass 5149 dfiota2 5181 dffun2 5228 dffun6f 5231 dffun4f 5234 dffun7 5245 dffun9 5247 funfn 5248 svrelfun 5283 imadiflem 5297 dffn2 5369 dffn3 5378 fintm 5403 dffn4 5446 dff1o4 5471 brprcneu 5510 eqfnfv3 5618 fnreseql 5629 fsn 5691 abrexco 5763 imaiun 5764 mpo2eqb 5987 elovmpo 6075 abexex 6130 releldm2 6189 fnmpo 6206 dftpos4 6267 tfrlem7 6321 0er 6572 eroveu 6629 erovlem 6630 map0e 6689 elixpconst 6709 domen 6754 reuen1 6804 xpf1o 6847 ssfilem 6878 finexdc 6905 pw1dc0el 6914 ssfirab 6936 sbthlemi10 6968 djuexb 7046 dmaddpq 7381 dmmulpq 7382 distrnqg 7389 enq0enq 7433 enq0tr 7436 nqnq0pi 7440 distrnq0 7461 prltlu 7489 prarloc 7505 genpdflem 7509 ltexprlemm 7602 ltexprlemlol 7604 ltexprlemupu 7606 ltexprlemdisj 7608 recexprlemdisj 7632 ltresr 7841 elnnz 9266 dfz2 9328 2rexuz 9585 eluz2b1 9604 elxr 9779 elixx1 9900 elioo2 9924 elioopnf 9970 elicopnf 9972 elfz1 10016 fzdifsuc 10084 fznn 10092 fzp1nel 10107 fznn0 10116 dfrp2 10267 redivap 10886 imdivap 10893 rexanre 11232 climreu 11308 prodmodc 11589 3dvdsdec 11873 3dvds2dec 11874 bezoutlembi 12009 nnwosdc 12043 isprm2 12120 isprm3 12121 isprm4 12122 pythagtriplem2 12269 elgz 12372 inffinp1 12433 isnsg4 13078 isring 13189 lss1d 13476 isbasis3g 13686 restsn 13820 lmbr 13853 txbas 13898 tx2cn 13910 elcncf1di 14206 dedekindicclemicc 14250 limcrcl 14267 bj-nnor 14626 bj-vprc 14788 ss1oel2o 14884 subctctexmid 14891 trirec0xor 14934 |
Copyright terms: Public domain | W3C validator |