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 387 pm5.32ri 451 mpan10 466 an31 554 an4 576 or4 761 ordir 807 andir 809 3anrot 972 3orrot 973 3ancoma 974 3orcomb 976 3ioran 982 3anbi123i 1177 3orbi123i 1178 3or6 1312 xorcom 1377 nfbii 1460 19.26-3an 1470 alnex 1486 19.42h 1674 19.42 1675 equsal 1714 equsalv 1780 sb6 1873 eeeanv 1920 sbbi 1946 sbco3xzyz 1960 sbcom2v 1972 sbel2x 1985 sb8eu 2026 sb8mo 2027 sb8euh 2036 eu1 2038 cbvmo 2053 mo3h 2066 sbmo 2072 eqcom 2166 abeq1 2274 cbvabw 2287 cbvab 2288 clelab 2290 nfceqi 2302 sbabel 2333 ralbii2 2474 rexbii2 2475 r2alf 2481 r2exf 2482 nfraldya 2499 nfrexdya 2500 r3al 2508 r19.41 2619 r19.42v 2621 ralcomf 2625 rexcomf 2626 reean 2632 3reeanv 2634 rabid2 2640 rabbi 2641 reubiia 2648 rmobiia 2653 reu5 2676 rmo5 2679 cbvralfw 2681 cbvralf 2682 cbvrexf 2683 cbvreu 2687 cbvrmo 2688 cbvralvw 2693 cbvrexvw 2694 vjust 2722 ceqsex3v 2763 ceqsex4v 2764 ceqsex8v 2766 eueq 2892 reu2 2909 reu6 2910 reu3 2911 rmo4 2914 rmo3f 2918 2rmorex 2927 cbvsbcw 2973 cbvsbc 2974 sbccomlem 3020 rmo3 3037 csbcow 3051 csbabg 3101 cbvralcsf 3102 cbvrexcsf 3103 cbvreucsf 3104 eqss 3152 uniiunlem 3226 ssequn1 3287 unss 3291 rexun 3297 ralunb 3298 elin3 3308 incom 3309 inass 3327 ssin 3339 ssddif 3351 unssdif 3352 difin 3354 invdif 3359 indif 3360 indi 3364 symdifxor 3383 disj3 3456 eldifpr 3597 rexsns 3609 reusn 3641 prss 3723 tpss 3732 eluni2 3787 elunirab 3796 uniun 3802 uni0b 3808 unissb 3813 elintrab 3830 ssintrab 3841 intun 3849 intpr 3850 iuncom 3866 iuncom4 3867 iunab 3906 ssiinf 3909 iinab 3921 iunin2 3923 iunun 3938 iunxun 3939 iunxiun 3941 sspwuni 3944 iinpw 3950 cbvdisj 3963 brun 4027 brin 4028 brdif 4029 dftr2 4076 inuni 4128 repizf2lem 4134 unidif0 4140 ssext 4193 pweqb 4195 otth2 4213 opelopabsbALT 4231 eqopab2b 4251 pwin 4254 unisuc 4385 elpwpwel 4447 sucexb 4468 elomssom 4576 xpiundi 4656 xpiundir 4657 poinxp 4667 soinxp 4668 seinxp 4669 inopab 4730 difopab 4731 raliunxp 4739 rexiunxp 4740 iunxpf 4746 cnvco 4783 dmiun 4807 dmuni 4808 dm0rn0 4815 brres 4884 dmres 4899 cnvsym 4981 asymref 4983 codir 4986 qfto 4987 cnvopab 4999 cnvdif 5004 rniun 5008 dminss 5012 imainss 5013 cnvcnvsn 5074 resco 5102 imaco 5103 rnco 5104 coiun 5107 coass 5116 ressn 5138 cnviinm 5139 xpcom 5144 funcnv 5243 funcnv3 5244 fncnv 5248 fun11 5249 fnres 5298 dfmpt3 5304 fnopabg 5305 fintm 5367 fin 5368 fores 5413 dff1o3 5432 fun11iun 5447 f11o 5459 f1ompt 5630 fsn 5651 imaiun 5722 isores2 5775 eqoprab2b 5891 opabex3d 6081 opabex3 6082 dfopab2 6149 dfoprab3s 6150 fmpox 6160 tpostpos 6223 dfsmo2 6246 qsid 6557 mapval2 6635 mapsncnv 6652 elixp2 6659 ixpin 6680 xpassen 6787 diffitest 6844 pw1dc0el 6868 supmoti 6949 eqinfti 6976 distrnqg 7319 ltbtwnnq 7348 distrnq0 7391 nqprrnd 7475 ltresr 7771 elznn0nn 9196 xrnemnf 9704 xrnepnf 9705 elioomnf 9895 elxrge0 9905 elfzuzb 9945 fzass4 9987 elfz2nn0 10037 elfzo2 10075 elfzo3 10088 lbfzo0 10106 fzind2 10164 dfrp2 10189 rexfiuz 10917 fisumcom2 11365 prodmodc 11505 fprodcom2fi 11553 infssuzex 11867 isbasis2g 12590 tgval2 12598 ntreq0 12679 txuni2 12803 isms2 13001 bdceq 13565 |
Copyright terms: Public domain | W3C validator |