Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3bitr4i | GIF version |
Description: A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
3bitr4i.1 | ⊢ (𝜑 ↔ 𝜓) |
3bitr4i.2 | ⊢ (𝜒 ↔ 𝜑) |
3bitr4i.3 | ⊢ (𝜃 ↔ 𝜓) |
Ref | Expression |
---|---|
3bitr4i | ⊢ (𝜒 ↔ 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr4i.2 | . 2 ⊢ (𝜒 ↔ 𝜑) | |
2 | 3bitr4i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 3bitr4i.3 | . . 3 ⊢ (𝜃 ↔ 𝜓) | |
4 | 2, 3 | bitr4i 186 | . 2 ⊢ (𝜑 ↔ 𝜃) |
5 | 1, 4 | 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: bibi2d 231 pm4.71 386 pm5.32ri 450 mpan10 465 an31 538 an4 560 or4 745 ordir 791 andir 793 3anrot 952 3orrot 953 3ancoma 954 3orcomb 956 3ioran 962 3anbi123i 1155 3orbi123i 1156 3or6 1286 xorcom 1351 nfbii 1434 19.26-3an 1444 alnex 1460 19.42h 1650 19.42 1651 equsal 1690 sb6 1842 eeeanv 1885 sbbi 1910 sbco3xzyz 1924 sbcom2v 1938 sbel2x 1951 sb8eu 1990 sb8mo 1991 sb8euh 2000 eu1 2002 cbvmo 2017 mo3h 2030 sbmo 2036 eqcom 2119 abeq1 2227 cbvab 2240 clelab 2242 nfceqi 2254 sbabel 2284 ralbii2 2422 rexbii2 2423 r2alf 2429 r2exf 2430 nfraldya 2446 nfrexdya 2447 r3al 2454 r19.41 2563 r19.42v 2565 ralcomf 2569 rexcomf 2570 reean 2576 3reeanv 2578 rabid2 2584 rabbi 2585 reubiia 2592 rmobiia 2597 reu5 2620 rmo5 2623 cbvralf 2625 cbvrexf 2626 cbvreu 2629 cbvrmo 2630 vjust 2661 ceqsex3v 2702 ceqsex4v 2703 ceqsex8v 2705 eueq 2828 reu2 2845 reu6 2846 reu3 2847 rmo4 2850 rmo3f 2854 2rmorex 2863 cbvsbc 2909 sbccomlem 2955 rmo3 2972 csbabg 3031 cbvralcsf 3032 cbvrexcsf 3033 cbvreucsf 3034 eqss 3082 uniiunlem 3155 ssequn1 3216 unss 3220 rexun 3226 ralunb 3227 elin3 3237 incom 3238 inass 3256 ssin 3268 ssddif 3280 unssdif 3281 difin 3283 invdif 3288 indif 3289 indi 3293 symdifxor 3312 disj3 3385 rexsns 3533 reusn 3564 prss 3646 tpss 3655 eluni2 3710 elunirab 3719 uniun 3725 uni0b 3731 unissb 3736 elintrab 3753 ssintrab 3764 intun 3772 intpr 3773 iuncom 3789 iuncom4 3790 iunab 3829 ssiinf 3832 iinab 3844 iunin2 3846 iunun 3861 iunxun 3862 iunxiun 3864 sspwuni 3867 iinpw 3873 cbvdisj 3886 brun 3949 brin 3950 brdif 3951 dftr2 3998 inuni 4050 repizf2lem 4055 unidif0 4061 ssext 4113 pweqb 4115 otth2 4133 opelopabsbALT 4151 eqopab2b 4171 pwin 4174 unisuc 4305 elpwpwel 4366 sucexb 4383 elnn 4489 xpiundi 4567 xpiundir 4568 poinxp 4578 soinxp 4579 seinxp 4580 inopab 4641 difopab 4642 raliunxp 4650 rexiunxp 4651 iunxpf 4657 cnvco 4694 dmiun 4718 dmuni 4719 dm0rn0 4726 brres 4795 dmres 4810 cnvsym 4892 asymref 4894 codir 4897 qfto 4898 cnvopab 4910 cnvdif 4915 rniun 4919 dminss 4923 imainss 4924 cnvcnvsn 4985 resco 5013 imaco 5014 rnco 5015 coiun 5018 coass 5027 ressn 5049 cnviinm 5050 xpcom 5055 funcnv 5154 funcnv3 5155 fncnv 5159 fun11 5160 fnres 5209 dfmpt3 5215 fnopabg 5216 fintm 5278 fin 5279 fores 5324 dff1o3 5341 fun11iun 5356 f11o 5368 f1ompt 5539 fsn 5560 imaiun 5629 isores2 5682 eqoprab2b 5797 opabex3d 5987 opabex3 5988 dfopab2 6055 dfoprab3s 6056 fmpox 6066 tpostpos 6129 dfsmo2 6152 qsid 6462 mapval2 6540 mapsncnv 6557 elixp2 6564 ixpin 6585 xpassen 6692 diffitest 6749 supmoti 6848 eqinfti 6875 distrnqg 7163 ltbtwnnq 7192 distrnq0 7235 nqprrnd 7319 ltresr 7615 elznn0nn 9026 xrnemnf 9519 xrnepnf 9520 elioomnf 9706 elxrge0 9716 elfzuzb 9755 fzass4 9797 elfz2nn0 9847 elfzo2 9882 elfzo3 9895 lbfzo0 9913 fzind2 9971 rexfiuz 10716 fisumcom2 11162 infssuzex 11554 isbasis2g 12123 tgval2 12131 ntreq0 12212 txuni2 12336 isms2 12534 bdceq 12936 |
Copyright terms: Public domain | W3C validator |