![]() |
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 679 orass 683 or32 686 dcan 841 dn1dc 866 an6 1215 excxor 1268 trubifal 1304 truxortru 1307 truxorfal 1308 falxortru 1309 falxorfal 1310 alrot4 1372 excom13 1576 sborv 1767 3exdistr 1789 4exdistr 1790 eeeanv 1805 ee4anv 1806 ee8anv 1807 sb3an 1829 elsb3 1849 elsb4 1850 sb9 1852 sbnf2 1854 sbco4 1880 2exsb 1882 sb8eu 1910 sb8euh 1920 sbmo 1956 2eu4 1990 2eu7 1991 r19.26-3 2437 rexcom13 2469 cbvreu 2525 ceqsex2 2588 ceqsex4v 2591 spc3gv 2639 ralrab2 2700 rexrab2 2702 reu2 2723 rmo4 2728 reu8 2731 rmo3 2843 dfss2 2928 ss2rab 3010 rabss 3011 ssrab 3012 undi 3179 undif3ss 3192 difin2 3193 dfnul2 3220 disj 3262 disjsn 3423 uni0c 3597 ssint 3622 iunss 3689 ssextss 3947 eqvinop 3971 opcom 3978 opeqsn 3980 opeqpr 3981 brabsb 3989 opelopabf 4002 opabm 4008 pofun 4040 sotritrieq 4053 uniuni 4149 ordsucim 4192 opeliunxp 4338 xpiundi 4341 brinxp2 4350 ssrel 4371 reliun 4401 cnvuni 4464 dmopab3 4491 opelres 4560 elres 4589 elsnres 4590 intirr 4654 ssrnres 4706 dminxp 4708 dfrel4v 4715 dmsnm 4729 rnco 4770 sb8iota 4817 dffun2 4855 dffun4f 4861 funco 4883 funcnveq 4905 fun11 4909 isarep1 4928 dff1o4 5077 dff1o6 5359 oprabid 5480 mpt22eqb 5552 ralrnmpt2 5557 rexrnmpt2 5558 opabex3d 5690 opabex3 5691 xporderlem 5793 tfr0 5878 tfrexlem 5889 frec0g 5922 nnaord 6018 ecid 6105 xpsnen 6231 xpcomco 6236 xpassen 6240 nqnq0 6424 opelreal 6726 elnn0 7959 elxr 8466 xrnepnf 8470 elfzuzb 8654 4fvwrd4 8767 elfzo2 8777 |
Copyright terms: Public domain | W3C validator |