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-mp 5 ax-1 6 ax-2 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 biancomi 268 imdistan 441 biadani 602 mpbiran 929 mpbiran2 930 3anrev 977 an6 1310 nfand 1555 19.33b2 1616 nf3 1656 nf4dc 1657 nf4r 1658 equsalh 1713 sb6x 1766 sb5f 1791 sbidm 1838 sb5 1874 sbanv 1876 sborv 1877 sbhb 1927 sb3an 1945 sbel2x 1985 sbal1yz 1988 sbexyz 1990 eu2 2057 2eu4 2106 cleqh 2264 cleqf 2331 dcne 2345 necon3bii 2372 ne3anior 2422 r2alf 2481 r2exf 2482 r19.23t 2571 r19.26-3 2594 r19.26m 2595 r19.43 2622 rabid2 2640 isset 2727 ralv 2738 rexv 2739 reuv 2740 rmov 2741 rexcom4b 2746 ceqsex4v 2764 ceqsex8v 2766 ceqsrexv 2851 ralrab2 2886 rexrab2 2888 reu2 2909 reu3 2911 reueq 2920 2reuswapdc 2925 reuind 2926 sbc3an 3007 rmo2ilem 3035 csbcow 3051 dfss2 3126 dfss3 3127 dfss3f 3129 ssabral 3208 rabss 3214 ssrabeq 3224 uniiunlem 3226 dfdif3 3227 ddifstab 3249 uncom 3261 inass 3327 indi 3364 difindiss 3371 difin2 3379 reupick3 3402 n0rf 3416 eq0 3422 eqv 3423 vss 3451 disj 3452 disj3 3456 undisj1 3461 undisj2 3462 exsnrex 3612 euabsn2 3639 euabsn 3640 prssg 3724 dfuni2 3785 unissb 3813 elint2 3825 ssint 3834 dfiin2g 3893 iunn0m 3920 iunxun 3939 iunxiun 3941 iinpw 3950 disjnim 3967 dftr2 4076 dftr5 4077 dftr3 4078 dftr4 4079 vnex 4107 inuni 4128 snelpw 4185 sspwb 4188 opelopabsb 4232 eusv2 4429 orddif 4518 onintexmid 4544 zfregfr 4545 tfi 4553 opthprc 4649 elxp3 4652 xpiundir 4657 elvv 4660 brinxp2 4665 relsn 4703 reliun 4719 inxp 4732 raliunxp 4739 rexiunxp 4740 cnvuni 4784 dm0rn0 4815 elrn 4841 ssdmres 4900 dfres2 4930 dfima2 4942 args 4967 cotr 4979 intasym 4982 asymref 4983 intirr 4984 cnv0 5001 xp11m 5036 cnvresima 5087 resco 5102 rnco 5104 coiun 5107 coass 5116 dfiota2 5148 dffun2 5192 dffun6f 5195 dffun4f 5198 dffun7 5209 dffun9 5211 funfn 5212 svrelfun 5247 imadiflem 5261 dffn2 5333 dffn3 5342 fintm 5367 dffn4 5410 dff1o4 5434 brprcneu 5473 eqfnfv3 5579 fnreseql 5589 fsn 5651 abrexco 5721 imaiun 5722 mpo2eqb 5942 elovmpo 6033 abexex 6086 releldm2 6145 fnmpo 6162 dftpos4 6222 tfrlem7 6276 0er 6526 eroveu 6583 erovlem 6584 map0e 6643 elixpconst 6663 domen 6708 reuen1 6758 xpf1o 6801 ssfilem 6832 finexdc 6859 pw1dc0el 6868 ssfirab 6890 sbthlemi10 6922 djuexb 7000 dmaddpq 7311 dmmulpq 7312 distrnqg 7319 enq0enq 7363 enq0tr 7366 nqnq0pi 7370 distrnq0 7391 prltlu 7419 prarloc 7435 genpdflem 7439 ltexprlemm 7532 ltexprlemlol 7534 ltexprlemupu 7536 ltexprlemdisj 7538 recexprlemdisj 7562 ltresr 7771 elnnz 9192 dfz2 9254 2rexuz 9511 eluz2b1 9530 elxr 9703 elixx1 9824 elioo2 9848 elioopnf 9894 elicopnf 9896 elfz1 9940 fzdifsuc 10006 fznn 10014 fzp1nel 10029 fznn0 10038 dfrp2 10189 redivap 10802 imdivap 10809 rexanre 11148 climreu 11224 prodmodc 11505 3dvdsdec 11787 3dvds2dec 11788 bezoutlembi 11923 isprm2 12028 isprm3 12029 isprm4 12030 pythagtriplem2 12177 inffinp1 12305 isbasis3g 12591 restsn 12727 lmbr 12760 txbas 12805 tx2cn 12817 elcncf1di 13113 dedekindicclemicc 13157 limcrcl 13174 bj-nnor 13458 bj-vprc 13619 ss1oel2o 13714 subctctexmid 13722 trirec0xor 13765 |
Copyright terms: Public domain | W3C validator |