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 173 | . 2 ⊢ (𝜓 ↔ 𝜃) |
5 | 1, 4 | bitri 173 | 1 ⊢ (𝜑 ↔ 𝜃) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: bibi1i 217 an32 496 orbi1i 680 orass 684 or32 687 dcan 842 dn1dc 867 an6 1216 excxor 1269 trubifal 1307 truxortru 1310 truxorfal 1311 falxortru 1312 falxorfal 1313 alrot4 1375 excom13 1579 sborv 1770 3exdistr 1792 4exdistr 1793 eeeanv 1808 ee4anv 1809 ee8anv 1810 sb3an 1832 elsb3 1852 elsb4 1853 sb9 1855 sbnf2 1857 sbco4 1883 2exsb 1885 sb8eu 1913 sb8euh 1923 sbmo 1959 2eu4 1993 2eu7 1994 r19.26-3 2443 rexcom13 2475 cbvreu 2531 ceqsex2 2594 ceqsex4v 2597 spc3gv 2645 ralrab2 2706 rexrab2 2708 reu2 2729 rmo4 2734 reu8 2737 rmo3 2849 dfss2 2934 ss2rab 3016 rabss 3017 ssrab 3018 undi 3185 undif3ss 3198 difin2 3199 dfnul2 3226 disj 3268 disjsn 3432 uni0c 3606 ssint 3631 iunss 3698 ssextss 3956 eqvinop 3980 opcom 3987 opeqsn 3989 opeqpr 3990 brabsb 3998 opelopabf 4011 opabm 4017 pofun 4049 sotritrieq 4062 uniuni 4183 ordsucim 4226 opeliunxp 4395 xpiundi 4398 brinxp2 4407 ssrel 4428 reliun 4458 cnvuni 4521 dmopab3 4548 opelres 4617 elres 4646 elsnres 4647 intirr 4711 ssrnres 4763 dminxp 4765 dfrel4v 4772 dmsnm 4786 rnco 4827 sb8iota 4874 dffun2 4912 dffun4f 4918 funco 4940 funcnveq 4962 fun11 4966 isarep1 4985 dff1o4 5134 dff1o6 5416 oprabid 5537 mpt22eqb 5610 ralrnmpt2 5615 rexrnmpt2 5616 opabex3d 5748 opabex3 5749 xporderlem 5852 tfr0 5937 tfrexlem 5948 frec0g 5983 nnaord 6082 ecid 6169 xpsnen 6295 xpcomco 6300 xpassen 6304 nqnq0 6539 opelreal 6904 pitoregt0 6925 elnn0 8183 elxr 8696 xrnepnf 8700 elfzuzb 8884 4fvwrd4 8997 elfzo2 9007 resqrexlemsqa 9622 |
Copyright terms: Public domain | W3C validator |