![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3bitr3g | Structured version Visualization version GIF version |
Description: More general version of 3bitr3i 300. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.) |
Ref | Expression |
---|---|
3bitr3g.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
3bitr3g.2 | ⊢ (𝜓 ↔ 𝜃) |
3bitr3g.3 | ⊢ (𝜒 ↔ 𝜏) |
Ref | Expression |
---|---|
3bitr3g | ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr3g.2 | . . 3 ⊢ (𝜓 ↔ 𝜃) | |
2 | 3bitr3g.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | bitr3id 284 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒)) |
4 | 3bitr3g.3 | . 2 ⊢ (𝜒 ↔ 𝜏) | |
5 | 3, 4 | bitrdi 286 | 1 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 |
This theorem is referenced by: notbid 317 cador 1602 cbvexdvaw 2035 cbvexdw 2330 cbvexd 2402 cbvrexdva 3228 raleq 3312 rexeqbidvvOLD 3322 cbvrexdva2 3333 rexeqf 3338 issetft 3477 dfsbcq2 3779 unineq 4279 iindif2 5085 reusv2 5407 rabxfrd 5421 opeqex 5504 eqbrrdv 5799 eqbrrdiv 5800 opelco2g 5874 opelcnvg 5887 ralrnmptw 7108 ralrnmpt 7110 fliftcnv 7323 eusvobj2 7416 br1steqg 8025 br2ndeqg 8026 ottpos 8251 smoiso 8392 ercnv 8755 ordiso2 9558 cantnfrescl 9719 cantnfp1lem3 9723 cantnflem1b 9729 cantnflem1 9732 cnfcom 9743 cnfcom3lem 9746 djulf1o 9955 djurf1o 9956 carden2 10030 cardeq0 10595 axpownd 10644 fpwwe2lem8 10681 fzen 13572 hasheq0 14380 incexc2 15842 divalglem4 16398 divalglem8 16402 divalgb 16406 sadadd 16467 sadass 16471 smuval2 16482 smumul 16493 isprm3 16684 vdwmc 16980 imasleval 17556 acsfn2 17676 invsym2 17779 yoniso 18310 pmtrfmvdn0 19460 dprd2d2 20044 cmpfi 23403 xkoinjcn 23682 tgpconncomp 24108 iscau3 25297 mbfimaopnlem 25675 ellimc3 25899 eldv 25918 eltayl 26387 atandm3 26906 noetasuplem4 27766 rmoxfrd 32421 opeldifid 32519 2ndpreima 32619 f1od2 32635 ordtconnlem1 33739 bnj1253 34862 usgrgt2cycl 34958 satfdm 35197 wl-dral1d 37226 wl-sb8eft 37246 wl-sb8et 37248 wl-equsb3 37251 wl-sb8eut 37273 wl-sb8eutv 37274 wl-issetft 37277 wl-ax11-lem8 37287 poimirlem2 37323 poimirlem16 37337 poimirlem18 37339 poimirlem21 37342 poimirlem22 37343 eqbrrdv2 38561 islpln5 39234 islvol5 39278 ntrneicls11 43757 radcnvrat 43988 trsbc 44216 iindif2f 44765 ichnreuop 47044 ichreuopeq 47045 pm5.32dav 48181 exp12bd 48183 aacllem 48549 |
Copyright terms: Public domain | W3C validator |