![]() |
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-1 5 ax-2 6 ax-mp 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 384 pm5.32ri 448 mpan10 463 an31 536 an4 558 or4 743 ordir 789 andir 791 3anrot 948 3orrot 949 3ancoma 950 3orcomb 952 3ioran 958 3anbi123i 1151 3orbi123i 1152 3or6 1282 xorcom 1347 nfbii 1430 19.26-3an 1440 alnex 1456 19.42h 1646 19.42 1647 equsal 1686 sb6 1838 eeeanv 1881 sbbi 1906 sbco3xzyz 1920 sbcom2v 1934 sbel2x 1947 sb8eu 1986 sb8mo 1987 sb8euh 1996 eu1 1998 cbvmo 2013 mo3h 2026 sbmo 2032 eqcom 2115 abeq1 2222 cbvab 2235 clelab 2237 nfceqi 2249 sbabel 2279 ralbii2 2417 rexbii2 2418 r2alf 2424 r2exf 2425 nfraldya 2441 nfrexdya 2442 r3al 2449 r19.41 2558 r19.42v 2560 ralcomf 2564 rexcomf 2565 reean 2571 3reeanv 2573 rabid2 2579 rabbi 2580 reubiia 2587 rmobiia 2592 reu5 2615 rmo5 2618 cbvralf 2620 cbvrexf 2621 cbvreu 2624 cbvrmo 2625 vjust 2656 ceqsex3v 2697 ceqsex4v 2698 ceqsex8v 2700 eueq 2822 reu2 2839 reu6 2840 reu3 2841 rmo4 2844 rmo3f 2848 2rmorex 2857 cbvsbc 2903 sbccomlem 2949 rmo3 2966 csbabg 3025 cbvralcsf 3026 cbvrexcsf 3027 cbvreucsf 3028 eqss 3076 uniiunlem 3149 ssequn1 3210 unss 3214 rexun 3220 ralunb 3221 elin3 3231 incom 3232 inass 3250 ssin 3262 ssddif 3274 unssdif 3275 difin 3277 invdif 3282 indif 3283 indi 3287 symdifxor 3306 disj3 3379 rexsns 3527 reusn 3558 prss 3640 tpss 3649 eluni2 3704 elunirab 3713 uniun 3719 uni0b 3725 unissb 3730 elintrab 3747 ssintrab 3758 intun 3766 intpr 3767 iuncom 3783 iuncom4 3784 iunab 3823 ssiinf 3826 iinab 3838 iunin2 3840 iunun 3855 iunxun 3856 iunxiun 3858 sspwuni 3861 iinpw 3867 cbvdisj 3880 brun 3939 brin 3940 brdif 3941 dftr2 3986 inuni 4038 repizf2lem 4043 unidif0 4049 ssext 4101 pweqb 4103 otth2 4121 opelopabsbALT 4139 eqopab2b 4159 pwin 4162 unisuc 4293 elpwpwel 4354 sucexb 4371 elnn 4477 xpiundi 4555 xpiundir 4556 poinxp 4566 soinxp 4567 seinxp 4568 inopab 4629 difopab 4630 raliunxp 4638 rexiunxp 4639 iunxpf 4645 cnvco 4682 dmiun 4706 dmuni 4707 dm0rn0 4714 brres 4781 dmres 4796 cnvsym 4878 asymref 4880 codir 4883 qfto 4884 cnvopab 4896 cnvdif 4901 rniun 4905 dminss 4909 imainss 4910 cnvcnvsn 4971 resco 4999 imaco 5000 rnco 5001 coiun 5004 coass 5013 ressn 5035 cnviinm 5036 xpcom 5041 funcnv 5140 funcnv3 5141 fncnv 5145 fun11 5146 fnres 5195 dfmpt3 5201 fnopabg 5202 fintm 5264 fin 5265 fores 5310 dff1o3 5327 fun11iun 5342 f11o 5354 f1ompt 5523 fsn 5544 imaiun 5613 isores2 5666 eqoprab2b 5781 opabex3d 5971 opabex3 5972 dfopab2 6039 dfoprab3s 6040 fmpox 6050 tpostpos 6113 dfsmo2 6136 qsid 6446 mapval2 6524 mapsncnv 6541 elixp2 6548 ixpin 6569 xpassen 6675 diffitest 6732 supmoti 6830 eqinfti 6857 distrnqg 7137 ltbtwnnq 7166 distrnq0 7209 nqprrnd 7293 ltresr 7568 elznn0nn 8966 xrnemnf 9451 xrnepnf 9452 elioomnf 9638 elxrge0 9648 elfzuzb 9687 fzass4 9729 elfz2nn0 9779 elfzo2 9814 elfzo3 9827 lbfzo0 9845 fzind2 9903 rexfiuz 10647 fisumcom2 11093 infssuzex 11484 isbasis2g 12049 tgval2 12057 ntreq0 12138 txuni2 12261 isms2 12437 bdceq 12723 |
Copyright terms: Public domain | W3C validator |