![]() |
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 176 | . 2 ⊢ (φ ↔ θ) |
5 | 1, 4 | bitri 173 | 1 ⊢ (χ ↔ θ) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: bibi2d 221 pm4.71 369 pm5.32ri 428 mpan10 443 an31 498 an4 520 or4 687 ordir 729 andir 731 dcbii 746 3anrot 889 3orrot 890 3ancoma 891 3orcomb 893 3ioran 899 3anbi123i 1092 3orbi123i 1093 3or6 1217 xorcom 1276 nfbii 1359 19.26-3an 1369 alnex 1385 19.42h 1574 19.42 1575 equsal 1612 sb6 1763 eeeanv 1805 sbbi 1830 sbco3xzyz 1844 sbcom2v 1858 sbel2x 1871 sb8eu 1910 sb8mo 1911 sb8euh 1920 eu1 1922 cbvmo 1937 mo3h 1950 sbmo 1956 eqcom 2039 abeq1 2144 cbvab 2157 clelab 2159 nfceqi 2171 sbabel 2200 ralbii2 2328 rexbii2 2329 r2alf 2335 r2exf 2336 nfraldya 2352 nfrexdya 2353 r3al 2360 r19.41 2459 r19.42v 2461 ralcomf 2465 rexcomf 2466 reean 2472 3reeanv 2474 rabid2 2480 rabbi 2481 reubiia 2488 rmobiia 2493 reu5 2516 rmo5 2519 cbvralf 2521 cbvrexf 2522 cbvreu 2525 cbvrmo 2526 vjust 2552 ceqsex3v 2590 ceqsex4v 2591 ceqsex8v 2593 eueq 2706 reu2 2723 reu6 2724 reu3 2725 rmo4 2728 2rmorex 2739 cbvsbc 2785 sbccomlem 2826 rmo3 2843 csbabg 2901 cbvralcsf 2902 cbvrexcsf 2903 cbvreucsf 2904 eqss 2954 uniiunlem 3022 ssequn1 3107 unss 3111 rexun 3117 ralunb 3118 elin3 3122 incom 3123 inass 3141 ssin 3153 nssinpss 3163 ssddif 3165 unssdif 3166 difin 3168 invdif 3173 indif 3174 indi 3178 symdifxor 3197 disj3 3266 rexsns 3400 reusn 3432 difsnpssim 3498 prss 3511 tpss 3520 eluni2 3575 elunirab 3584 uniun 3590 uni0b 3596 unissb 3601 elintrab 3618 ssintrab 3629 intun 3637 intpr 3638 iuncom 3654 iuncom4 3655 iunab 3694 ssiinf 3697 iinab 3709 iunin2 3711 iunun 3725 iunxun 3726 iunxiun 3727 sspwuni 3730 iinpw 3733 cbvdisj 3746 brun 3801 brin 3802 brdif 3803 dftr2 3847 inuni 3900 repizf2lem 3905 unidif0 3911 ssext 3948 pweqb 3950 otth2 3969 opelopabsbALT 3987 eqopab2b 4007 pwin 4010 unisuc 4116 sucexb 4189 elnn 4271 xpiundi 4341 xpiundir 4342 poinxp 4352 soinxp 4353 seinxp 4354 inopab 4411 difopab 4412 raliunxp 4420 rexiunxp 4421 iunxpf 4427 cnvco 4463 dmiun 4487 dmuni 4488 dm0rn0 4495 brres 4561 dmres 4575 cnvsym 4651 asymref 4653 codir 4656 qfto 4657 cnvopab 4669 cnvdif 4673 rniun 4677 dminss 4681 imainss 4682 cnvcnvsn 4740 resco 4768 imaco 4769 rnco 4770 coiun 4773 coass 4782 ressn 4801 cnviinm 4802 xpcom 4807 funcnv 4903 funcnv3 4904 fncnv 4908 fun11 4909 fnres 4958 dfmpt3 4964 fnopabg 4965 fintm 5018 fin 5019 fores 5058 dff1o3 5075 fun11iun 5090 f11o 5102 f1ompt 5263 fsn 5278 imaiun 5342 isores2 5396 eqoprab2b 5505 opabex3d 5690 opabex3 5691 dfopab2 5757 dfoprab3s 5758 fmpt2x 5768 tpostpos 5820 dfsmo2 5843 qsid 6107 xpassen 6240 distrnqg 6371 ltbtwnnq 6399 distrnq0 6442 nqprrnd 6526 ltresr 6736 elznn0nn 8035 xrnemnf 8469 xrnepnf 8470 elioomnf 8607 elxrge0 8617 elfzuzb 8654 fzass4 8695 elfz2nn0 8743 elfzo2 8777 elfzo3 8789 lbfzo0 8807 fzind2 8865 bdceq 9297 |
Copyright terms: Public domain | W3C validator |