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 452 mpan10 471 an31 559 an4 581 or4 766 ordir 812 andir 814 3anrot 978 3orrot 979 3ancoma 980 3orcomb 982 3ioran 988 3anbi123i 1183 3orbi123i 1184 3or6 1318 xorcom 1383 nfbii 1466 19.26-3an 1476 alnex 1492 19.42h 1680 19.42 1681 equsal 1720 equsalv 1786 sb6 1879 eeeanv 1926 sbbi 1952 sbco3xzyz 1966 sbcom2v 1978 sbel2x 1991 sb8eu 2032 sb8mo 2033 sb8euh 2042 eu1 2044 cbvmo 2059 mo3h 2072 sbmo 2078 eqcom 2172 abeq1 2280 cbvabw 2293 cbvab 2294 clelab 2296 nfceqi 2308 sbabel 2339 ralbii2 2480 rexbii2 2481 r2alf 2487 r2exf 2488 nfraldya 2505 nfrexdya 2506 r3al 2514 r19.41 2625 r19.42v 2627 ralcomf 2631 rexcomf 2632 reean 2638 3reeanv 2640 rabid2 2646 rabbi 2647 reubiia 2654 rmobiia 2659 reu5 2682 rmo5 2685 cbvralfw 2687 cbvrexfw 2688 cbvralf 2689 cbvrexf 2690 cbvreu 2694 cbvrmo 2695 cbvralvw 2700 cbvrexvw 2701 vjust 2731 ceqsex3v 2772 ceqsex4v 2773 ceqsex8v 2775 eueq 2901 reu2 2918 reu6 2919 reu3 2920 rmo4 2923 rmo3f 2927 2rmorex 2936 cbvsbcw 2982 cbvsbc 2983 sbccomlem 3029 rmo3 3046 csbcow 3060 csbabg 3110 cbvralcsf 3111 cbvrexcsf 3112 cbvreucsf 3113 eqss 3162 uniiunlem 3236 ssequn1 3297 unss 3301 rexun 3307 ralunb 3308 elin3 3318 incom 3319 inass 3337 ssin 3349 ssddif 3361 unssdif 3362 difin 3364 invdif 3369 indif 3370 indi 3374 symdifxor 3393 disj3 3467 eldifpr 3610 rexsns 3622 reusn 3654 prss 3736 tpss 3745 eluni2 3800 elunirab 3809 uniun 3815 uni0b 3821 unissb 3826 elintrab 3843 ssintrab 3854 intun 3862 intpr 3863 iuncom 3879 iuncom4 3880 iunab 3919 ssiinf 3922 iinab 3934 iunin2 3936 iunun 3951 iunxun 3952 iunxiun 3954 sspwuni 3957 iinpw 3963 cbvdisj 3976 brun 4040 brin 4041 brdif 4042 dftr2 4089 inuni 4141 repizf2lem 4147 unidif0 4153 ssext 4206 pweqb 4208 otth2 4226 opelopabsbALT 4244 eqopab2b 4264 pwin 4267 unisuc 4398 elpwpwel 4460 sucexb 4481 elomssom 4589 xpiundi 4669 xpiundir 4670 poinxp 4680 soinxp 4681 seinxp 4682 inopab 4743 difopab 4744 raliunxp 4752 rexiunxp 4753 iunxpf 4759 cnvco 4796 dmiun 4820 dmuni 4821 dm0rn0 4828 brres 4897 dmres 4912 cnvsym 4994 asymref 4996 codir 4999 qfto 5000 cnvopab 5012 cnvdif 5017 rniun 5021 dminss 5025 imainss 5026 cnvcnvsn 5087 resco 5115 imaco 5116 rnco 5117 coiun 5120 coass 5129 ressn 5151 cnviinm 5152 xpcom 5157 funcnv 5259 funcnv3 5260 fncnv 5264 fun11 5265 fnres 5314 dfmpt3 5320 fnopabg 5321 fintm 5383 fin 5384 fores 5429 dff1o3 5448 fun11iun 5463 f11o 5475 f1ompt 5647 fsn 5668 imaiun 5739 isores2 5792 eqoprab2b 5911 opabex3d 6100 opabex3 6101 dfopab2 6168 dfoprab3s 6169 fmpox 6179 tpostpos 6243 dfsmo2 6266 qsid 6578 mapval2 6656 mapsncnv 6673 elixp2 6680 ixpin 6701 xpassen 6808 diffitest 6865 pw1dc0el 6889 supmoti 6970 eqinfti 6997 distrnqg 7349 ltbtwnnq 7378 distrnq0 7421 nqprrnd 7505 ltresr 7801 elznn0nn 9226 xrnemnf 9734 xrnepnf 9735 elioomnf 9925 elxrge0 9935 elfzuzb 9975 fzass4 10018 elfz2nn0 10068 elfzo2 10106 elfzo3 10119 lbfzo0 10137 fzind2 10195 dfrp2 10220 rexfiuz 10953 fisumcom2 11401 prodmodc 11541 fprodcom2fi 11589 infssuzex 11904 infpn2 12411 isbasis2g 12837 tgval2 12845 ntreq0 12926 txuni2 13050 isms2 13248 bdceq 13877 |
Copyright terms: Public domain | W3C validator |