![]() |
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 688 ordir 730 andir 732 dcbii 747 3anrot 890 3orrot 891 3ancoma 892 3orcomb 894 3ioran 900 3anbi123i 1093 3orbi123i 1094 3or6 1218 xorcom 1279 nfbii 1362 19.26-3an 1372 alnex 1388 19.42h 1577 19.42 1578 equsal 1615 sb6 1766 eeeanv 1808 sbbi 1833 sbco3xzyz 1847 sbcom2v 1861 sbel2x 1874 sb8eu 1913 sb8mo 1914 sb8euh 1923 eu1 1925 cbvmo 1940 mo3h 1953 sbmo 1959 eqcom 2042 abeq1 2147 cbvab 2160 clelab 2162 nfceqi 2174 sbabel 2203 ralbii2 2334 rexbii2 2335 r2alf 2341 r2exf 2342 nfraldya 2358 nfrexdya 2359 r3al 2366 r19.41 2465 r19.42v 2467 ralcomf 2471 rexcomf 2472 reean 2478 3reeanv 2480 rabid2 2486 rabbi 2487 reubiia 2494 rmobiia 2499 reu5 2522 rmo5 2525 cbvralf 2527 cbvrexf 2528 cbvreu 2531 cbvrmo 2532 vjust 2558 ceqsex3v 2596 ceqsex4v 2597 ceqsex8v 2599 eueq 2712 reu2 2729 reu6 2730 reu3 2731 rmo4 2734 2rmorex 2745 cbvsbc 2791 sbccomlem 2832 rmo3 2849 csbabg 2907 cbvralcsf 2908 cbvrexcsf 2909 cbvreucsf 2910 eqss 2960 uniiunlem 3028 ssequn1 3113 unss 3117 rexun 3123 ralunb 3124 elin3 3128 incom 3129 inass 3147 ssin 3159 nssinpss 3169 ssddif 3171 unssdif 3172 difin 3174 invdif 3179 indif 3180 indi 3184 symdifxor 3203 disj3 3272 rexsns 3409 reusn 3441 difsnpssim 3507 prss 3520 tpss 3529 eluni2 3584 elunirab 3593 uniun 3599 uni0b 3605 unissb 3610 elintrab 3627 ssintrab 3638 intun 3646 intpr 3647 iuncom 3663 iuncom4 3664 iunab 3703 ssiinf 3706 iinab 3718 iunin2 3720 iunun 3734 iunxun 3735 iunxiun 3736 sspwuni 3739 iinpw 3742 cbvdisj 3755 brun 3810 brin 3811 brdif 3812 dftr2 3856 inuni 3909 repizf2lem 3914 unidif0 3920 ssext 3957 pweqb 3959 otth2 3978 opelopabsbALT 3996 eqopab2b 4016 pwin 4019 unisuc 4150 sucexb 4223 elnn 4328 xpiundi 4398 xpiundir 4399 poinxp 4409 soinxp 4410 seinxp 4411 inopab 4468 difopab 4469 raliunxp 4477 rexiunxp 4478 iunxpf 4484 cnvco 4520 dmiun 4544 dmuni 4545 dm0rn0 4552 brres 4618 dmres 4632 cnvsym 4708 asymref 4710 codir 4713 qfto 4714 cnvopab 4726 cnvdif 4730 rniun 4734 dminss 4738 imainss 4739 cnvcnvsn 4797 resco 4825 imaco 4826 rnco 4827 coiun 4830 coass 4839 ressn 4858 cnviinm 4859 xpcom 4864 funcnv 4960 funcnv3 4961 fncnv 4965 fun11 4966 fnres 5015 dfmpt3 5021 fnopabg 5022 fintm 5075 fin 5076 fores 5115 dff1o3 5132 fun11iun 5147 f11o 5159 f1ompt 5320 fsn 5335 imaiun 5399 isores2 5453 eqoprab2b 5563 opabex3d 5748 opabex3 5749 dfopab2 5815 dfoprab3s 5816 fmpt2x 5826 tpostpos 5879 dfsmo2 5902 qsid 6171 xpassen 6304 diffitest 6344 distrnqg 6485 ltbtwnnq 6514 distrnq0 6557 nqprrnd 6641 ltresr 6915 elznn0nn 8259 xrnemnf 8699 xrnepnf 8700 elioomnf 8837 elxrge0 8847 elfzuzb 8884 fzass4 8925 elfz2nn0 8973 elfzo2 9007 elfzo3 9019 lbfzo0 9037 fzind2 9095 bdceq 9962 |
Copyright terms: Public domain | W3C validator |