![]() |
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 187 | . 2 ⊢ (𝜑 ↔ 𝜃) |
5 | 1, 4 | bitri 184 | 1 ⊢ (𝜒 ↔ 𝜃) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: bibi2d 232 pm4.71 389 pm5.32ri 455 mpan10 474 an31 564 an4 586 or4 772 ordir 818 andir 820 3anrot 985 3orrot 986 3ancoma 987 3orcomb 989 3ioran 995 3anbi123i 1190 3orbi123i 1191 3or6 1334 xorcom 1399 nfbii 1484 19.26-3an 1494 alnex 1510 19.42h 1698 19.42 1699 equsal 1738 equsalv 1804 sb6 1898 eeeanv 1945 sbbi 1971 sbco3xzyz 1985 sbcom2v 1997 sbel2x 2010 sb8eu 2051 sb8mo 2052 sb8euh 2061 eu1 2063 cbvmo 2078 mo3h 2091 sbmo 2097 eqcom 2191 abeq1 2299 cbvabw 2312 cbvab 2313 clelab 2315 nfceqi 2328 sbabel 2359 ralbii2 2500 rexbii2 2501 r2alf 2507 r2exf 2508 nfraldya 2525 nfrexdya 2526 r3al 2534 r19.41 2645 r19.42v 2647 ralcomf 2651 rexcomf 2652 reean 2659 3reeanv 2661 rabid2 2667 rabbi 2668 reubiia 2675 rmobiia 2680 reu5 2703 rmo5 2706 cbvralfw 2708 cbvrexfw 2709 cbvralf 2710 cbvrexf 2711 cbvreu 2716 cbvrmo 2717 cbvralvw 2722 cbvrexvw 2723 vjust 2753 ceqsex3v 2794 ceqsex4v 2795 ceqsex8v 2797 eueq 2923 reu2 2940 reu6 2941 reu3 2942 rmo4 2945 rmo3f 2949 2rmorex 2958 cbvsbcw 3005 cbvsbc 3006 sbccomlem 3052 rmo3 3069 csbcow 3083 csbabg 3133 cbvralcsf 3134 cbvrexcsf 3135 cbvreucsf 3136 eqss 3185 uniiunlem 3259 ssequn1 3320 unss 3324 rexun 3330 ralunb 3331 elin3 3341 incom 3342 inass 3360 ssin 3372 ssddif 3384 unssdif 3385 difin 3387 invdif 3392 indif 3393 indi 3397 symdifxor 3416 disj3 3490 eldifpr 3634 rexsns 3646 reusn 3678 prss 3763 tpss 3773 eluni2 3828 elunirab 3837 uniun 3843 uni0b 3849 unissb 3854 elintrab 3871 ssintrab 3882 intun 3890 intpr 3891 iuncom 3907 iuncom4 3908 iunab 3948 ssiinf 3951 iinab 3963 iunin2 3965 iunun 3980 iunxun 3981 iunxiun 3983 sspwuni 3986 iinpw 3992 cbvdisj 4005 brun 4069 brin 4070 brdif 4071 dftr2 4118 inuni 4173 repizf2lem 4179 unidif0 4185 ssext 4239 pweqb 4241 otth2 4259 opelopabsbALT 4277 eqopab2b 4297 pwin 4300 unisuc 4431 elpwpwel 4493 sucexb 4514 elomssom 4622 xpiundi 4702 xpiundir 4703 poinxp 4713 soinxp 4714 seinxp 4715 inopab 4777 difopab 4778 raliunxp 4786 rexiunxp 4787 iunxpf 4793 cnvco 4830 dmiun 4854 dmuni 4855 dm0rn0 4862 brres 4931 dmres 4946 restidsing 4981 cnvsym 5030 asymref 5032 codir 5035 qfto 5036 cnvopab 5048 cnvdif 5053 rniun 5057 dminss 5061 imainss 5062 cnvcnvsn 5123 resco 5151 imaco 5152 rnco 5153 coiun 5156 coass 5165 ressn 5187 cnviinm 5188 xpcom 5193 funcnv 5296 funcnv3 5297 fncnv 5301 fun11 5302 fnres 5351 dfmpt3 5357 fnopabg 5358 fintm 5420 fin 5421 fores 5466 dff1o3 5486 fun11iun 5501 f11o 5513 f1ompt 5688 fsn 5709 imaiun 5782 isores2 5835 eqoprab2b 5955 opabex3d 6147 opabex3 6148 dfopab2 6215 dfoprab3s 6216 fmpox 6226 tpostpos 6290 dfsmo2 6313 qsid 6627 mapval2 6705 mapsncnv 6722 elixp2 6729 ixpin 6750 xpassen 6857 diffitest 6916 pw1dc0el 6940 supmoti 7023 eqinfti 7050 distrnqg 7417 ltbtwnnq 7446 distrnq0 7489 nqprrnd 7573 ltresr 7869 elznn0nn 9298 xrnemnf 9809 xrnepnf 9810 elioomnf 10000 elxrge0 10010 elfzuzb 10051 fzass4 10094 elfz2nn0 10144 elfzo2 10182 elfzo3 10195 lbfzo0 10213 fzind2 10271 dfrp2 10296 rexfiuz 11033 fisumcom2 11481 prodmodc 11621 fprodcom2fi 11669 infssuzex 11985 4sqlem12 12437 infpn2 12510 xpsfrnel 12823 xpscf 12826 islmod 13624 isbasis2g 14022 tgval2 14028 ntreq0 14109 txuni2 14233 isms2 14431 bdceq 15072 |
Copyright terms: Public domain | W3C validator |