![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3bitr4i | Unicode version |
Description: A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
3bitr4i.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
3bitr4i.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
3bitr4i.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3bitr4i |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr4i.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3bitr4i.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 3bitr4i.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | bitr4i 186 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | 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: bibi2d 231 pm4.71 382 pm5.32ri 444 mpan10 459 an31 532 an4 554 or4 726 ordir 769 andir 771 dcbii 788 3anrot 932 3orrot 933 3ancoma 934 3orcomb 936 3ioran 942 3anbi123i 1135 3orbi123i 1136 3or6 1266 xorcom 1331 nfbii 1414 19.26-3an 1424 alnex 1440 19.42h 1629 19.42 1630 equsal 1669 sb6 1821 eeeanv 1863 sbbi 1888 sbco3xzyz 1902 sbcom2v 1916 sbel2x 1929 sb8eu 1968 sb8mo 1969 sb8euh 1978 eu1 1980 cbvmo 1995 mo3h 2008 sbmo 2014 eqcom 2097 abeq1 2204 cbvab 2217 clelab 2219 nfceqi 2231 sbabel 2261 ralbii2 2399 rexbii2 2400 r2alf 2406 r2exf 2407 nfraldya 2423 nfrexdya 2424 r3al 2431 r19.41 2536 r19.42v 2538 ralcomf 2542 rexcomf 2543 reean 2549 3reeanv 2551 rabid2 2557 rabbi 2558 reubiia 2565 rmobiia 2570 reu5 2593 rmo5 2596 cbvralf 2598 cbvrexf 2599 cbvreu 2602 cbvrmo 2603 vjust 2634 ceqsex3v 2675 ceqsex4v 2676 ceqsex8v 2678 eueq 2800 reu2 2817 reu6 2818 reu3 2819 rmo4 2822 rmo3f 2826 2rmorex 2835 cbvsbc 2881 sbccomlem 2927 rmo3 2944 csbabg 3003 cbvralcsf 3004 cbvrexcsf 3005 cbvreucsf 3006 eqss 3054 uniiunlem 3124 ssequn1 3185 unss 3189 rexun 3195 ralunb 3196 elin3 3206 incom 3207 inass 3225 ssin 3237 ssddif 3249 unssdif 3250 difin 3252 invdif 3257 indif 3258 indi 3262 symdifxor 3281 disj3 3354 rexsns 3502 reusn 3533 prss 3615 tpss 3624 eluni2 3679 elunirab 3688 uniun 3694 uni0b 3700 unissb 3705 elintrab 3722 ssintrab 3733 intun 3741 intpr 3742 iuncom 3758 iuncom4 3759 iunab 3798 ssiinf 3801 iinab 3813 iunin2 3815 iunun 3830 iunxun 3831 iunxiun 3832 sspwuni 3835 iinpw 3841 cbvdisj 3854 brun 3913 brin 3914 brdif 3915 dftr2 3960 inuni 4012 repizf2lem 4017 unidif0 4023 ssext 4072 pweqb 4074 otth2 4092 opelopabsbALT 4110 eqopab2b 4130 pwin 4133 unisuc 4264 elpwpwel 4325 sucexb 4342 elnn 4448 xpiundi 4525 xpiundir 4526 poinxp 4536 soinxp 4537 seinxp 4538 inopab 4599 difopab 4600 raliunxp 4608 rexiunxp 4609 iunxpf 4615 cnvco 4652 dmiun 4676 dmuni 4677 dm0rn0 4684 brres 4751 dmres 4766 cnvsym 4848 asymref 4850 codir 4853 qfto 4854 cnvopab 4866 cnvdif 4871 rniun 4875 dminss 4879 imainss 4880 cnvcnvsn 4941 resco 4969 imaco 4970 rnco 4971 coiun 4974 coass 4983 ressn 5005 cnviinm 5006 xpcom 5011 funcnv 5109 funcnv3 5110 fncnv 5114 fun11 5115 fnres 5164 dfmpt3 5170 fnopabg 5171 fintm 5231 fin 5232 fores 5277 dff1o3 5294 fun11iun 5309 f11o 5321 f1ompt 5489 fsn 5508 imaiun 5577 isores2 5630 eqoprab2b 5745 opabex3d 5930 opabex3 5931 dfopab2 5997 dfoprab3s 5998 fmpt2x 6008 tpostpos 6067 dfsmo2 6090 qsid 6397 mapval2 6475 mapsncnv 6492 elixp2 6499 ixpin 6520 xpassen 6626 diffitest 6683 supmoti 6768 eqinfti 6795 distrnqg 7043 ltbtwnnq 7072 distrnq0 7115 nqprrnd 7199 ltresr 7473 elznn0nn 8862 xrnemnf 9347 xrnepnf 9348 elioomnf 9534 elxrge0 9544 elfzuzb 9583 fzass4 9625 elfz2nn0 9675 elfzo2 9710 elfzo3 9723 lbfzo0 9741 fzind2 9799 rexfiuz 10553 fisumcom2 10997 infssuzex 11388 isbasis2g 11911 tgval2 11919 ntreq0 12000 isms2 12256 bdceq 12457 |
Copyright terms: Public domain | W3C validator |