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 553 an4 575 or4 760 ordir 806 andir 808 3anrot 967 3orrot 968 3ancoma 969 3orcomb 971 3ioran 977 3anbi123i 1170 3orbi123i 1171 3or6 1301 xorcom 1366 nfbii 1449 19.26-3an 1459 alnex 1475 19.42h 1665 19.42 1666 equsal 1705 sb6 1858 eeeanv 1903 sbbi 1930 sbco3xzyz 1944 sbcom2v 1958 sbel2x 1971 sb8eu 2010 sb8mo 2011 sb8euh 2020 eu1 2022 cbvmo 2037 mo3h 2050 sbmo 2056 eqcom 2139 abeq1 2247 cbvabw 2260 cbvab 2261 clelab 2263 nfceqi 2275 sbabel 2305 ralbii2 2443 rexbii2 2444 r2alf 2450 r2exf 2451 nfraldya 2467 nfrexdya 2468 r3al 2475 r19.41 2584 r19.42v 2586 ralcomf 2590 rexcomf 2591 reean 2597 3reeanv 2599 rabid2 2605 rabbi 2606 reubiia 2613 rmobiia 2618 reu5 2641 rmo5 2644 cbvralf 2646 cbvrexf 2647 cbvreu 2650 cbvrmo 2651 vjust 2682 ceqsex3v 2723 ceqsex4v 2724 ceqsex8v 2726 eueq 2850 reu2 2867 reu6 2868 reu3 2869 rmo4 2872 rmo3f 2876 2rmorex 2885 cbvsbcw 2931 cbvsbc 2932 sbccomlem 2978 rmo3 2995 csbabg 3056 cbvralcsf 3057 cbvrexcsf 3058 cbvreucsf 3059 eqss 3107 uniiunlem 3180 ssequn1 3241 unss 3245 rexun 3251 ralunb 3252 elin3 3262 incom 3263 inass 3281 ssin 3293 ssddif 3305 unssdif 3306 difin 3308 invdif 3313 indif 3314 indi 3318 symdifxor 3337 disj3 3410 rexsns 3558 reusn 3589 prss 3671 tpss 3680 eluni2 3735 elunirab 3744 uniun 3750 uni0b 3756 unissb 3761 elintrab 3778 ssintrab 3789 intun 3797 intpr 3798 iuncom 3814 iuncom4 3815 iunab 3854 ssiinf 3857 iinab 3869 iunin2 3871 iunun 3886 iunxun 3887 iunxiun 3889 sspwuni 3892 iinpw 3898 cbvdisj 3911 brun 3974 brin 3975 brdif 3976 dftr2 4023 inuni 4075 repizf2lem 4080 unidif0 4086 ssext 4138 pweqb 4140 otth2 4158 opelopabsbALT 4176 eqopab2b 4196 pwin 4199 unisuc 4330 elpwpwel 4391 sucexb 4408 elnn 4514 xpiundi 4592 xpiundir 4593 poinxp 4603 soinxp 4604 seinxp 4605 inopab 4666 difopab 4667 raliunxp 4675 rexiunxp 4676 iunxpf 4682 cnvco 4719 dmiun 4743 dmuni 4744 dm0rn0 4751 brres 4820 dmres 4835 cnvsym 4917 asymref 4919 codir 4922 qfto 4923 cnvopab 4935 cnvdif 4940 rniun 4944 dminss 4948 imainss 4949 cnvcnvsn 5010 resco 5038 imaco 5039 rnco 5040 coiun 5043 coass 5052 ressn 5074 cnviinm 5075 xpcom 5080 funcnv 5179 funcnv3 5180 fncnv 5184 fun11 5185 fnres 5234 dfmpt3 5240 fnopabg 5241 fintm 5303 fin 5304 fores 5349 dff1o3 5366 fun11iun 5381 f11o 5393 f1ompt 5564 fsn 5585 imaiun 5654 isores2 5707 eqoprab2b 5822 opabex3d 6012 opabex3 6013 dfopab2 6080 dfoprab3s 6081 fmpox 6091 tpostpos 6154 dfsmo2 6177 qsid 6487 mapval2 6565 mapsncnv 6582 elixp2 6589 ixpin 6610 xpassen 6717 diffitest 6774 supmoti 6873 eqinfti 6900 distrnqg 7188 ltbtwnnq 7217 distrnq0 7260 nqprrnd 7344 ltresr 7640 elznn0nn 9061 xrnemnf 9557 xrnepnf 9558 elioomnf 9744 elxrge0 9754 elfzuzb 9793 fzass4 9835 elfz2nn0 9885 elfzo2 9920 elfzo3 9933 lbfzo0 9951 fzind2 10009 rexfiuz 10754 fisumcom2 11200 infssuzex 11631 isbasis2g 12201 tgval2 12209 ntreq0 12290 txuni2 12414 isms2 12612 bdceq 13029 |
Copyright terms: Public domain | W3C validator |