![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3bitri | GIF 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 184 | . 2 ⊢ (𝜓 ↔ 𝜃) |
5 | 1, 4 | bitri 184 | 1 ⊢ (𝜑 ↔ 𝜃) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 |
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: bibi1i 228 an32 562 orbi1i 764 orass 768 or32 771 dcan 934 dn1dc 961 an6 1331 excxor 1388 trubifal 1426 truxortru 1429 truxorfal 1430 falxortru 1431 falxorfal 1432 alrot4 1496 excom13 1699 sborv 1901 3exdistr 1926 4exdistr 1927 eeeanv 1944 ee4anv 1945 ee8anv 1946 sb3an 1969 sb9 1990 sbnf2 1992 sbco4 2018 2exsb 2020 sb8eu 2050 sb8euh 2060 sbmo 2096 2eu4 2130 2eu7 2131 elsb1 2166 elsb2 2167 r19.26-3 2619 rexcom13 2655 cbvreu 2715 ceqsex2 2791 ceqsex4v 2794 spc3gv 2844 ralrab2 2916 rexrab2 2918 reu2 2939 rmo4 2944 reu8 2947 rmo3f 2948 sbc3an 3038 rmo3 3068 dfss2 3158 ss2rab 3245 rabss 3246 ssrab 3247 dfdif3 3259 undi 3397 undif3ss 3410 difin2 3411 dfnul2 3438 disj 3485 disjsn 3668 snssb 3739 uni0c 3849 ssint 3874 iunss 3941 ssextss 4234 eqvinop 4257 opcom 4264 opeqsn 4266 opeqpr 4267 brabsb 4275 opelopabf 4288 opabm 4294 pofun 4326 sotritrieq 4339 uniuni 4465 ordsucim 4513 opeliunxp 4695 xpiundi 4698 brinxp2 4707 ssrel 4728 reliun 4761 cnvuni 4827 dmopab3 4854 opelres 4926 elres 4957 elsnres 4958 intirr 5029 ssrnres 5085 dminxp 5087 dfrel4v 5094 dmsnm 5108 rnco 5149 sb8iota 5199 dffun2 5240 dffun4f 5246 funco 5270 funcnveq 5293 fun11 5297 isarep1 5316 dff1o4 5483 dff1o6 5792 oprabid 5922 mpo2eqb 6000 ralrnmpo 6005 rexrnmpo 6006 opabex3d 6139 opabex3 6140 xporderlem 6249 f1od2 6253 tfr0dm 6340 tfrexlem 6352 frec0g 6415 nnaord 6527 ecid 6615 mptelixpg 6751 elixpsn 6752 mapsnen 6828 xpsnen 6838 xpcomco 6843 xpassen 6847 exmidontriimlem3 7239 nqnq0 7457 opelreal 7843 pitoregt0 7865 elnn0 9195 elxnn0 9258 elxr 9793 xrnepnf 9795 elfzuzb 10036 4fvwrd4 10157 elfzo2 10167 resqrexlemsqa 11050 fisumcom2 11463 modfsummod 11483 fprodcom2fi 11651 nnwosdc 12057 isprm2 12134 isprm4 12136 pythagtriplem2 12283 isnsg2 13107 isnsg4 13116 dfrhm2 13464 ntreq0 14015 txbas 14141 metrest 14389 |
Copyright terms: Public domain | W3C validator |