![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bitr4i | GIF version |
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr4i.1 | ⊢ (φ ↔ ψ) |
bitr4i.2 | ⊢ (χ ↔ ψ) |
Ref | Expression |
---|---|
bitr4i | ⊢ (φ ↔ χ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr4i.1 | . 2 ⊢ (φ ↔ ψ) | |
2 | bitr4i.2 | . . 3 ⊢ (χ ↔ ψ) | |
3 | 2 | bicomi 123 | . 2 ⊢ (ψ ↔ χ) |
4 | 1, 3 | 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: 3bitr2i 197 3bitr2ri 198 3bitr4i 201 3bitr4ri 202 imdistan 418 mpbiran 846 mpbiran2 847 3anrev 894 an6 1215 nfand 1457 19.33b2 1517 nf3 1556 nf4dc 1557 nf4r 1558 equsalh 1611 sb6x 1659 sb5f 1682 sbidm 1728 sb5 1764 sbanv 1766 sborv 1767 sbhb 1813 sb3an 1829 sbel2x 1871 sbal1yz 1874 sbexyz 1876 eu2 1941 2eu4 1990 cleqh 2134 cleqf 2198 dcne 2211 necon3bii 2237 ne3anior 2287 r2alf 2335 r2exf 2336 r19.23t 2417 r19.26-3 2437 r19.26m 2438 r19.43 2462 rabid2 2480 isset 2555 ralv 2565 rexv 2566 reuv 2567 rmov 2568 rexcom4b 2573 ceqsex4v 2591 ceqsex8v 2593 ceqsrexv 2668 ralrab2 2700 rexrab2 2702 reu2 2723 reu3 2725 reueq 2732 2reuswapdc 2737 reuind 2738 rmo2ilem 2841 dfss2 2928 dfss3 2929 dfss3f 2931 ssabral 3005 rabss 3011 ssrabeq 3020 uniiunlem 3022 uncom 3081 inass 3141 nsspssun 3164 indi 3178 difindiss 3185 difin2 3193 reupick3 3216 n0rf 3227 eq0 3233 eqv 3234 vss 3258 disj 3262 disj3 3266 undisj1 3273 undisj2 3274 exsnrex 3404 euabsn2 3430 euabsn 3431 prssg 3512 dfuni2 3573 unissb 3601 elint2 3613 ssint 3622 dfiin2g 3681 iunn0m 3708 iunxun 3726 iunxiun 3727 iinpw 3733 dftr2 3847 dftr5 3848 dftr3 3849 dftr4 3850 vprc 3879 inuni 3900 snelpw 3940 sspwb 3943 opelopabsb 3988 eusv2 4155 tfi 4248 opthprc 4334 elxp3 4337 xpiundir 4342 elvv 4345 brinxp2 4350 relsn 4386 reliun 4401 inxp 4413 raliunxp 4420 rexiunxp 4421 cnvuni 4464 dm0rn0 4495 elrn 4520 ssdmres 4576 dfres2 4601 dfima2 4613 args 4637 cotr 4649 intasym 4652 asymref 4653 intirr 4654 cnv0 4670 xp11m 4702 cnvresima 4753 resco 4768 rnco 4770 coiun 4773 coass 4782 dfiota2 4811 dffun2 4855 dffun6f 4858 dffun4f 4861 dffun7 4871 dffun9 4873 funfn 4874 svrelfun 4907 imadiflem 4921 dffn2 4990 dffn3 4996 fintm 5018 dffn4 5055 dff1o4 5077 brprcneu 5114 eqfnfv3 5210 fnreseql 5220 fsn 5278 abrexco 5341 imaiun 5342 mpt22eqb 5552 elovmpt2 5643 abexex 5695 releldm2 5753 fnmpt2 5770 dftpos4 5819 tfrlem7 5874 0er 6076 eroveu 6133 erovlem 6134 domen 6168 reuen1 6217 ssfiexmid 6254 dmaddpq 6363 dmmulpq 6364 distrnqg 6371 enq0enq 6414 enq0tr 6417 nqnq0pi 6421 distrnq0 6442 prltlu 6470 prarloc 6486 genpdflem 6490 ltexprlemm 6574 ltexprlemlol 6576 ltexprlemupu 6578 ltexprlemdisj 6580 recexprlemdisj 6602 ltresr 6736 elnnz 8031 dfz2 8089 2rexuz 8301 eluz2b1 8315 elxr 8466 elixx1 8536 elioo2 8560 elioopnf 8606 elicopnf 8608 elfz1 8649 fzdifsuc 8713 fznn 8721 fzp1nel 8736 fznn0 8744 redivap 9102 imdivap 9109 dcdc 9236 bj-vprc 9351 |
Copyright terms: Public domain | W3C validator |