![]() |
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 183 | . 2 ⊢ (𝜓 ↔ 𝜃) |
5 | 1, 4 | bitri 183 | 1 ⊢ (𝜑 ↔ 𝜃) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 |
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: bibi1i 227 an32 534 orbi1i 735 orass 739 or32 742 dcan 901 dn1dc 927 an6 1282 excxor 1339 trubifal 1377 truxortru 1380 truxorfal 1381 falxortru 1382 falxorfal 1383 alrot4 1445 excom13 1650 sborv 1844 3exdistr 1867 4exdistr 1868 eeeanv 1883 ee4anv 1884 ee8anv 1885 sb3an 1907 elsb3 1927 elsb4 1928 sb9 1930 sbnf2 1932 sbco4 1958 2exsb 1960 sb8eu 1988 sb8euh 1998 sbmo 2034 2eu4 2068 2eu7 2069 r19.26-3 2536 rexcom13 2570 cbvreu 2626 ceqsex2 2697 ceqsex4v 2700 spc3gv 2749 ralrab2 2818 rexrab2 2820 reu2 2841 rmo4 2846 reu8 2849 rmo3f 2850 sbc3an 2938 rmo3 2968 dfss2 3052 ss2rab 3139 rabss 3140 ssrab 3141 dfdif3 3152 undi 3290 undif3ss 3303 difin2 3304 dfnul2 3331 disj 3377 disjsn 3551 uni0c 3728 ssint 3753 iunss 3820 ssextss 4102 eqvinop 4125 opcom 4132 opeqsn 4134 opeqpr 4135 brabsb 4143 opelopabf 4156 opabm 4162 pofun 4194 sotritrieq 4207 uniuni 4332 ordsucim 4376 opeliunxp 4554 xpiundi 4557 brinxp2 4566 ssrel 4587 reliun 4620 cnvuni 4685 dmopab3 4712 opelres 4782 elres 4813 elsnres 4814 intirr 4883 ssrnres 4939 dminxp 4941 dfrel4v 4948 dmsnm 4962 rnco 5003 sb8iota 5053 dffun2 5091 dffun4f 5097 funco 5121 funcnveq 5144 fun11 5148 isarep1 5167 dff1o4 5331 dff1o6 5631 oprabid 5757 mpo2eqb 5834 ralrnmpo 5839 rexrnmpo 5840 opabex3d 5973 opabex3 5974 xporderlem 6082 f1od2 6086 tfr0dm 6173 tfrexlem 6185 frec0g 6248 nnaord 6359 ecid 6446 mptelixpg 6582 elixpsn 6583 mapsnen 6659 xpsnen 6668 xpcomco 6673 xpassen 6677 nqnq0 7197 opelreal 7562 pitoregt0 7584 elnn0 8883 elxnn0 8946 elxr 9456 xrnepnf 9458 elfzuzb 9693 4fvwrd4 9810 elfzo2 9820 resqrexlemsqa 10688 fisumcom2 11099 modfsummod 11119 isprm2 11644 isprm4 11646 ntreq0 12144 txbas 12269 metrest 12495 |
Copyright terms: Public domain | W3C validator |