![]() |
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 130 | . 2 ⊢ (𝜓 ↔ 𝜒) |
4 | 1, 3 | bitri 182 | 1 ⊢ (𝜑 ↔ 𝜒) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: 3bitr2i 206 3bitr2ri 207 3bitr4i 210 3bitr4ri 211 imdistan 433 mpbiran 882 mpbiran2 883 3anrev 930 an6 1253 nfand 1501 19.33b2 1561 nf3 1600 nf4dc 1601 nf4r 1602 equsalh 1655 sb6x 1703 sb5f 1726 sbidm 1773 sb5 1809 sbanv 1811 sborv 1812 sbhb 1858 sb3an 1874 sbel2x 1916 sbal1yz 1919 sbexyz 1921 eu2 1986 2eu4 2035 cleqh 2179 cleqf 2243 dcne 2257 necon3bii 2284 ne3anior 2334 r2alf 2384 r2exf 2385 r19.23t 2468 r19.26-3 2488 r19.26m 2489 r19.43 2513 rabid2 2531 isset 2606 ralv 2617 rexv 2618 reuv 2619 rmov 2620 rexcom4b 2625 ceqsex4v 2643 ceqsex8v 2645 ceqsrexv 2726 ralrab2 2758 rexrab2 2760 reu2 2781 reu3 2783 reueq 2790 2reuswapdc 2795 reuind 2796 sbc3an 2876 rmo2ilem 2904 dfss2 2989 dfss3 2990 dfss3f 2992 ssabral 3066 rabss 3072 ssrabeq 3081 uniiunlem 3083 ddifstab 3105 uncom 3117 inass 3183 indi 3218 difindiss 3225 difin2 3233 reupick3 3256 n0rf 3267 eq0 3273 eqv 3274 vss 3298 disj 3299 disj3 3303 undisj1 3308 undisj2 3309 exsnrex 3443 euabsn2 3469 euabsn 3470 prssg 3550 dfuni2 3611 unissb 3639 elint2 3651 ssint 3660 dfiin2g 3719 iunn0m 3746 iunxun 3764 iunxiun 3765 iinpw 3771 dftr2 3885 dftr5 3886 dftr3 3887 dftr4 3888 vprc 3917 inuni 3938 snelpw 3976 sspwb 3979 opelopabsb 4023 eusv2 4215 orddif 4298 onintexmid 4323 zfregfr 4324 tfi 4331 opthprc 4417 elxp3 4420 xpiundir 4425 elvv 4428 brinxp2 4433 relsn 4471 reliun 4486 inxp 4498 raliunxp 4505 rexiunxp 4506 cnvuni 4549 dm0rn0 4580 elrn 4605 ssdmres 4661 dfres2 4688 dfima2 4700 args 4724 cotr 4736 intasym 4739 asymref 4740 intirr 4741 cnv0 4757 xp11m 4789 cnvresima 4840 resco 4855 rnco 4857 coiun 4860 coass 4869 dfiota2 4898 dffun2 4942 dffun6f 4945 dffun4f 4948 dffun7 4958 dffun9 4960 funfn 4961 svrelfun 4995 imadiflem 5009 dffn2 5078 dffn3 5084 fintm 5106 dffn4 5143 dff1o4 5165 brprcneu 5202 eqfnfv3 5299 fnreseql 5309 fsn 5367 abrexco 5430 imaiun 5431 mpt22eqb 5641 elovmpt2 5732 abexex 5784 releldm2 5842 fnmpt2 5859 dftpos4 5912 tfrlem7 5966 0er 6206 eroveu 6263 erovlem 6264 domen 6298 reuen1 6348 xpf1o 6385 ssfilem 6410 dmaddpq 6631 dmmulpq 6632 distrnqg 6639 enq0enq 6683 enq0tr 6686 nqnq0pi 6690 distrnq0 6711 prltlu 6739 prarloc 6755 genpdflem 6759 ltexprlemm 6852 ltexprlemlol 6854 ltexprlemupu 6856 ltexprlemdisj 6858 recexprlemdisj 6882 ltresr 7069 elnnz 8442 dfz2 8501 2rexuz 8751 eluz2b1 8769 elxr 8928 elixx1 8996 elioo2 9020 elioopnf 9066 elicopnf 9068 elfz1 9110 fzdifsuc 9174 fznn 9182 fzp1nel 9197 fznn0 9206 redivap 9899 imdivap 9906 rexanre 10244 climreu 10274 3dvdsdec 10409 3dvds2dec 10410 bezoutlembi 10538 isprm2 10643 isprm3 10644 isprm4 10645 dcdc 10723 bj-vprc 10845 |
Copyright terms: Public domain | W3C validator |