| 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 11242 cau4 11369 sumeq2 11612 fisumcom2 11691 fprodcom2fi 11879 dvdsflip 12104 bitsmod 12209 bitscmp 12211 divgcdcoprm0 12365 hashdvds 12485 4sqlem12 12667 imasaddfnlemg 13088 issgrpv 13178 issgrpn0 13179 mndpropd 13214 ismhm 13235 mhmpropd 13240 issubm2 13247 grppropd 13291 grpinvcnv 13342 conjghm 13554 conjnmzb 13558 ghmpropd 13561 cmnpropd 13573 ablpropd 13574 eqgabl 13608 rngpropd 13659 issrg 13669 ringpropd 13742 crngpropd 13743 opprnzrbg 13889 subrngpropd 13920 resrhm2b 13953 subrgpropd 13957 rhmpropd 13958 opprdomnbg 13978 lmodprop2d 14052 islssm 14061 islssmg 14062 lsspropdg 14135 df2idl2rng 14212 tpspropd 14450 tgss2 14493 lmbr2 14628 txcnmpt 14687 txhmeo 14733 blininf 14838 blres 14848 xmeterval 14849 xmspropd 14891 mspropd 14892 metequiv 14909 xmetxpbl 14922 limcdifap 15076 lgsquadlem1 15496 lgsquadlem2 15497 cbvrald 15657 bj-indeq 15798 |
| Copyright terms: Public domain | W3C validator |