![]() |
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 131 | . 2 ⊢ (𝜓 ↔ 𝜒) |
4 | 1, 3 | bitri 183 | 1 ⊢ (𝜑 ↔ 𝜒) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3bitr2i 207 3bitr2ri 208 3bitr4i 211 3bitr4ri 212 imdistan 436 biadani 582 mpbiran 892 mpbiran2 893 3anrev 940 an6 1267 nfand 1515 19.33b2 1576 nf3 1615 nf4dc 1616 nf4r 1617 equsalh 1672 sb6x 1720 sb5f 1743 sbidm 1790 sb5 1826 sbanv 1828 sborv 1829 sbhb 1876 sb3an 1892 sbel2x 1934 sbal1yz 1937 sbexyz 1939 eu2 2004 2eu4 2053 cleqh 2199 cleqf 2264 dcne 2278 necon3bii 2305 ne3anior 2355 r2alf 2411 r2exf 2412 r19.23t 2498 r19.26-3 2521 r19.26m 2522 r19.43 2547 rabid2 2565 isset 2647 ralv 2658 rexv 2659 reuv 2660 rmov 2661 rexcom4b 2666 ceqsex4v 2684 ceqsex8v 2686 ceqsrexv 2769 ralrab2 2802 rexrab2 2804 reu2 2825 reu3 2827 reueq 2836 2reuswapdc 2841 reuind 2842 sbc3an 2922 rmo2ilem 2950 dfss2 3036 dfss3 3037 dfss3f 3039 ssabral 3115 rabss 3121 ssrabeq 3130 uniiunlem 3132 dfdif3 3133 ddifstab 3155 uncom 3167 inass 3233 indi 3270 difindiss 3277 difin2 3285 reupick3 3308 n0rf 3322 eq0 3328 eqv 3329 vss 3357 disj 3358 disj3 3362 undisj1 3367 undisj2 3368 exsnrex 3513 euabsn2 3539 euabsn 3540 prssg 3624 dfuni2 3685 unissb 3713 elint2 3725 ssint 3734 dfiin2g 3793 iunn0m 3820 iunxun 3839 iunxiun 3840 iinpw 3849 disjnim 3866 dftr2 3968 dftr5 3969 dftr3 3970 dftr4 3971 vnex 3999 inuni 4020 snelpw 4073 sspwb 4076 opelopabsb 4120 eusv2 4316 orddif 4400 onintexmid 4425 zfregfr 4426 tfi 4434 opthprc 4528 elxp3 4531 xpiundir 4536 elvv 4539 brinxp2 4544 relsn 4582 reliun 4598 inxp 4611 raliunxp 4618 rexiunxp 4619 cnvuni 4663 dm0rn0 4694 elrn 4720 ssdmres 4777 dfres2 4807 dfima2 4819 args 4844 cotr 4856 intasym 4859 asymref 4860 intirr 4861 cnv0 4878 xp11m 4913 cnvresima 4964 resco 4979 rnco 4981 coiun 4984 coass 4993 dfiota2 5025 dffun2 5069 dffun6f 5072 dffun4f 5075 dffun7 5086 dffun9 5088 funfn 5089 svrelfun 5124 imadiflem 5138 dffn2 5210 dffn3 5219 fintm 5244 dffn4 5287 dff1o4 5309 brprcneu 5346 eqfnfv3 5452 fnreseql 5462 fsn 5524 abrexco 5592 imaiun 5593 mpo2eqb 5812 elovmpo 5903 abexex 5955 releldm2 6013 fnmpo 6030 dftpos4 6090 tfrlem7 6144 0er 6393 eroveu 6450 erovlem 6451 map0e 6510 elixpconst 6530 domen 6575 reuen1 6625 xpf1o 6667 ssfilem 6698 finexdc 6725 ssfirab 6750 sbthlemi10 6782 djuexb 6844 dmaddpq 7088 dmmulpq 7089 distrnqg 7096 enq0enq 7140 enq0tr 7143 nqnq0pi 7147 distrnq0 7168 prltlu 7196 prarloc 7212 genpdflem 7216 ltexprlemm 7309 ltexprlemlol 7311 ltexprlemupu 7313 ltexprlemdisj 7315 recexprlemdisj 7339 ltresr 7526 elnnz 8916 dfz2 8975 2rexuz 9227 eluz2b1 9245 elxr 9404 elixx1 9521 elioo2 9545 elioopnf 9591 elicopnf 9593 elfz1 9636 fzdifsuc 9702 fznn 9710 fzp1nel 9725 fznn0 9734 redivap 10487 imdivap 10494 rexanre 10832 climreu 10905 3dvdsdec 11357 3dvds2dec 11358 bezoutlembi 11486 isprm2 11591 isprm3 11592 isprm4 11593 inffinp1 11734 isbasis3g 11995 restsn 12131 lmbr 12163 txbas 12208 tx2cn 12220 elcncf1di 12479 limcrcl 12509 dcdc 12550 bj-vprc 12675 ss1oel2o 12774 |
Copyright terms: Public domain | W3C validator |