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-mp 5 ax-1 6 ax-2 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 552 orbi1i 753 orass 757 or32 760 dcan 923 dn1dc 949 an6 1310 excxor 1367 trubifal 1405 truxortru 1408 truxorfal 1409 falxortru 1410 falxorfal 1411 alrot4 1473 excom13 1676 sborv 1877 3exdistr 1902 4exdistr 1903 eeeanv 1920 ee4anv 1921 ee8anv 1922 sb3an 1945 sb9 1966 sbnf2 1968 sbco4 1994 2exsb 1996 sb8eu 2026 sb8euh 2036 sbmo 2072 2eu4 2106 2eu7 2107 elsb3 2142 elsb4 2143 r19.26-3 2594 rexcom13 2629 cbvreu 2687 ceqsex2 2761 ceqsex4v 2764 spc3gv 2814 ralrab2 2886 rexrab2 2888 reu2 2909 rmo4 2914 reu8 2917 rmo3f 2918 sbc3an 3007 rmo3 3037 dfss2 3126 ss2rab 3213 rabss 3214 ssrab 3215 dfdif3 3227 undi 3365 undif3ss 3378 difin2 3379 dfnul2 3406 disj 3452 disjsn 3632 uni0c 3809 ssint 3834 iunss 3901 ssextss 4192 eqvinop 4215 opcom 4222 opeqsn 4224 opeqpr 4225 brabsb 4233 opelopabf 4246 opabm 4252 pofun 4284 sotritrieq 4297 uniuni 4423 ordsucim 4471 opeliunxp 4653 xpiundi 4656 brinxp2 4665 ssrel 4686 reliun 4719 cnvuni 4784 dmopab3 4811 opelres 4883 elres 4914 elsnres 4915 intirr 4984 ssrnres 5040 dminxp 5042 dfrel4v 5049 dmsnm 5063 rnco 5104 sb8iota 5154 dffun2 5192 dffun4f 5198 funco 5222 funcnveq 5245 fun11 5249 isarep1 5268 dff1o4 5434 dff1o6 5738 oprabid 5865 mpo2eqb 5942 ralrnmpo 5947 rexrnmpo 5948 opabex3d 6081 opabex3 6082 xporderlem 6190 f1od2 6194 tfr0dm 6281 tfrexlem 6293 frec0g 6356 nnaord 6468 ecid 6555 mptelixpg 6691 elixpsn 6692 mapsnen 6768 xpsnen 6778 xpcomco 6783 xpassen 6787 exmidontriimlem3 7170 nqnq0 7373 opelreal 7759 pitoregt0 7781 elnn0 9107 elxnn0 9170 elxr 9703 xrnepnf 9705 elfzuzb 9945 4fvwrd4 10065 elfzo2 10075 resqrexlemsqa 10952 fisumcom2 11365 modfsummod 11385 fprodcom2fi 11553 isprm2 12028 isprm4 12030 pythagtriplem2 12177 ntreq0 12679 txbas 12805 metrest 13053 |
Copyright terms: Public domain | W3C validator |