Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3bitri | Unicode version |
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
3bitri.1 | |
3bitri.2 | |
3bitri.3 |
Ref | Expression |
---|---|
3bitri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitri.1 | . 2 | |
2 | 3bitri.2 | . . 3 | |
3 | 3bitri.3 | . . 3 | |
4 | 2, 3 | bitri 182 | . 2 |
5 | 1, 4 | bitri 182 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: bibi1i 226 an32 526 orbi1i 712 orass 716 or32 719 dcan 875 dn1dc 901 an6 1252 excxor 1309 trubifal 1347 truxortru 1350 truxorfal 1351 falxortru 1352 falxorfal 1353 alrot4 1415 excom13 1619 sborv 1811 3exdistr 1833 4exdistr 1834 eeeanv 1849 ee4anv 1850 ee8anv 1851 sb3an 1873 elsb3 1893 elsb4 1894 sb9 1896 sbnf2 1898 sbco4 1924 2exsb 1926 sb8eu 1954 sb8euh 1964 sbmo 2000 2eu4 2034 2eu7 2035 r19.26-3 2487 rexcom13 2519 cbvreu 2575 ceqsex2 2639 ceqsex4v 2642 spc3gv 2690 ralrab2 2757 rexrab2 2759 reu2 2780 rmo4 2785 reu8 2788 sbc3an 2875 rmo3 2905 dfss2 2988 ss2rab 3070 rabss 3071 ssrab 3072 undi 3212 undif3ss 3225 difin2 3226 dfnul2 3253 disj 3292 disjsn 3454 uni0c 3627 ssint 3652 iunss 3719 ssextss 3975 eqvinop 3998 opcom 4005 opeqsn 4007 opeqpr 4008 brabsb 4016 opelopabf 4029 opabm 4035 pofun 4067 sotritrieq 4080 uniuni 4201 ordsucim 4244 opeliunxp 4413 xpiundi 4416 brinxp2 4425 ssrel 4446 reliun 4476 cnvuni 4539 dmopab3 4566 opelres 4635 elres 4664 elsnres 4665 intirr 4731 ssrnres 4783 dminxp 4785 dfrel4v 4792 dmsnm 4806 rnco 4847 sb8iota 4894 dffun2 4932 dffun4f 4938 funco 4960 funcnveq 4982 fun11 4986 isarep1 5005 dff1o4 5154 dff1o6 5436 oprabid 5557 mpt22eqb 5630 ralrnmpt2 5635 rexrnmpt2 5636 opabex3d 5768 opabex3 5769 xporderlem 5872 f1od2 5876 tfr0 5960 tfrexlem 5971 frec0g 6006 nnaord 6105 ecid 6192 xpsnen 6318 xpcomco 6323 xpassen 6327 nqnq0 6631 opelreal 6996 pitoregt0 7017 elnn0 8290 elxr 8850 xrnepnf 8854 elfzuzb 9039 4fvwrd4 9150 elfzo2 9160 resqrexlemsqa 9910 isprm2 10499 isprm4 10501 |
Copyright terms: Public domain | W3C validator |