| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > 3bitr4g | GIF version | ||
| Description: More general version of 3bitr4i 212. Useful for converting definitions in a formula. (Contributed by NM, 5-Aug-1993.) |
| Ref | Expression |
|---|---|
| 3bitr4g.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| 3bitr4g.2 | ⊢ (𝜃 ↔ 𝜓) |
| 3bitr4g.3 | ⊢ (𝜏 ↔ 𝜒) |
| Ref | Expression |
|---|---|
| 3bitr4g | ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3bitr4g.2 | . . 3 ⊢ (𝜃 ↔ 𝜓) | |
| 2 | 3bitr4g.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 3 | 1, 2 | bitrid 192 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒)) |
| 4 | 3bitr4g.3 | . 2 ⊢ (𝜏 ↔ 𝜒) | |
| 5 | 3, 4 | bitr4di 198 | 1 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ↔ 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: bibi1d 233 pm5.32rd 451 orbi1d 792 stbid 833 dcbid 839 pm4.14dc 891 orbididc 955 3orbi123d 1323 3anbi123d 1324 xorbi2d 1399 xorbi1d 1400 nfbidf 1561 drnf1 1755 drnf2 1756 drsb1 1821 sbal2 2047 eubidh 2059 eubid 2060 mobidh 2087 mobid 2088 eqeq1 2211 eqeq2 2214 eleq1w 2265 eleq2w 2266 eleq1 2267 eleq2 2268 cbvabw 2327 eqabdv 2333 nfceqdf 2346 drnfc1 2364 drnfc2 2365 neeq1 2388 neeq2 2389 neleq1 2474 neleq2 2475 dfrex2dc 2496 ralbida 2499 rexbida 2500 ralbidv2 2507 rexbidv2 2508 ralbid2 2509 rexbid2 2510 r19.21t 2580 r19.23t 2612 reubida 2687 rmobida 2692 raleqf 2697 rexeqf 2698 reueq1f 2699 rmoeq1f 2700 cbvraldva2 2744 cbvrexdva2 2745 dfsbcq 2999 sbceqbid 3004 sbcbi2 3048 sbcbid 3055 eqsbc2 3058 sbcabel 3079 sbnfc2 3153 ssconb 3305 uneq1 3319 ineq1 3366 difin2 3434 reuun2 3455 reldisj 3511 undif4 3522 disjssun 3523 sbcssg 3568 eltpg 3677 raltpg 3685 rextpg 3686 r19.12sn 3698 opeq1 3818 opeq2 3819 intmin4 3912 dfiun2g 3958 iindif2m 3994 iinin2m 3995 breq 4045 breq1 4046 breq2 4047 treq 4147 opthg2 4282 poeq1 4345 soeq1 4361 frforeq1 4389 freq1 4390 frforeq2 4391 freq2 4392 frforeq3 4393 weeq1 4402 weeq2 4403 ordeq 4418 limeq 4423 rabxfrd 4515 iunpw 4526 opthprc 4725 releq 4756 sbcrel 4760 eqrel 4763 eqrelrel 4775 xpiindim 4814 brcnvg 4858 brresg 4966 resieq 4968 xpcanm 5121 xpcan2m 5122 dmsnopg 5153 dfco2a 5182 cnvpom 5224 cnvsom 5225 iotaeq 5239 sniota 5261 sbcfung 5294 fneq1 5361 fneq2 5362 feq1 5407 feq2 5408 feq3 5409 sbcfng 5422 sbcfg 5423 f1eq1 5475 f1eq2 5476 f1eq3 5477 foeq1 5493 foeq2 5494 foeq3 5495 f1oeq1 5509 f1oeq2 5510 f1oeq3 5511 fun11iun 5542 mpteqb 5669 dffo3 5726 fmptco 5745 dff13 5836 f1imaeq 5843 f1eqcocnv 5859 fliftcnv 5863 isoeq1 5869 isoeq2 5870 isoeq3 5871 isoeq4 5872 isoeq5 5873 isocnv2 5880 acexmid 5942 fnotovb 5987 mpoeq123 6003 ottposg 6340 dmtpos 6341 smoeq 6375 nnacan 6597 nnmcan 6604 ereq1 6626 ereq2 6627 elecg 6659 ereldm 6664 ixpiinm 6810 enfi 6969 elfi2 7073 fipwssg 7080 ctssdccl 7212 tapeq1 7363 tapeq2 7364 creur 9031 eqreznegel 9734 ltxr 9896 icoshftf1o 10112 elfzm11 10212 elfzomelpfzo 10358 nn0ennn 10576 nnesq 10802 rexfiuz 11271 cau4 11398 sumeq2 11641 fisumcom2 11720 fprodcom2fi 11908 dvdsflip 12133 bitsmod 12238 bitscmp 12240 divgcdcoprm0 12394 hashdvds 12514 4sqlem12 12696 imasaddfnlemg 13117 issgrpv 13207 issgrpn0 13208 mndpropd 13243 ismhm 13264 mhmpropd 13269 issubm2 13276 grppropd 13320 grpinvcnv 13371 conjghm 13583 conjnmzb 13587 ghmpropd 13590 cmnpropd 13602 ablpropd 13603 eqgabl 13637 rngpropd 13688 issrg 13698 ringpropd 13771 crngpropd 13772 opprnzrbg 13918 subrngpropd 13949 resrhm2b 13982 subrgpropd 13986 rhmpropd 13987 opprdomnbg 14007 lmodprop2d 14081 islssm 14090 islssmg 14091 lsspropdg 14164 df2idl2rng 14241 tpspropd 14479 tgss2 14522 lmbr2 14657 txcnmpt 14716 txhmeo 14762 blininf 14867 blres 14877 xmeterval 14878 xmspropd 14920 mspropd 14921 metequiv 14938 xmetxpbl 14951 limcdifap 15105 lgsquadlem1 15525 lgsquadlem2 15526 cbvrald 15686 bj-indeq 15827 |
| Copyright terms: Public domain | W3C validator |