| 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 301. 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 285 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒)) |
| 4 | 3bitr3g.3 | . 2 ⊢ (𝜒 ↔ 𝜏) | |
| 5 | 3, 4 | bitrdi 287 | 1 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: notbid 318 cador 1608 cbvexdvaw 2038 cbvexdw 2341 cbvexd 2413 cbvrexdva 3240 raleq 3323 rexeqbidvvOLD 3337 cbvrexdva2 3349 rexeqf 3354 cbvexeqsetf 3495 dfsbcq2 3791 unineq 4288 iindif2 5077 reusv2 5403 rabxfrd 5417 opeqex 5503 eqbrrdv 5803 eqbrrdiv 5804 opelco2g 5878 opelcnvg 5891 ralrnmptw 7114 ralrnmpt 7116 fliftcnv 7331 eusvobj2 7423 br1steqg 8036 br2ndeqg 8037 ottpos 8261 smoiso 8402 ercnv 8766 ordiso2 9555 cantnfrescl 9716 cantnfp1lem3 9720 cantnflem1b 9726 cantnflem1 9729 cnfcom 9740 cnfcom3lem 9743 djulf1o 9952 djurf1o 9953 carden2 10027 cardeq0 10592 axpownd 10641 fpwwe2lem8 10678 fzen 13581 hasheq0 14402 incexc2 15874 divalglem4 16433 divalglem8 16437 divalgb 16441 sadadd 16504 sadass 16508 smuval2 16519 smumul 16530 isprm3 16720 vdwmc 17016 imasleval 17586 acsfn2 17706 invsym2 17807 yoniso 18330 pmtrfmvdn0 19480 dprd2d2 20064 cmpfi 23416 xkoinjcn 23695 tgpconncomp 24121 iscau3 25312 mbfimaopnlem 25690 ellimc3 25914 eldv 25933 eltayl 26401 atandm3 26921 noetasuplem4 27781 rmoxfrd 32512 opeldifid 32612 2ndpreima 32717 f1od2 32732 ordtconnlem1 33923 bnj1253 35031 usgrgt2cycl 35135 satfdm 35374 wl-dral1d 37532 wl-sb8eft 37552 wl-sb8et 37554 wl-equsb3 37557 wl-sb8eut 37579 wl-sb8eutv 37580 wl-issetft 37583 wl-ax11-lem8 37593 poimirlem2 37629 poimirlem16 37643 poimirlem18 37645 poimirlem21 37648 poimirlem22 37649 eqbrrdv2 38864 islpln5 39537 islvol5 39581 ntrneicls11 44103 radcnvrat 44333 trsbc 44560 iindif2f 45165 ichnreuop 47459 ichreuopeq 47460 pm5.32dav 48714 exp12bd 48716 reuxfr1dd 48726 aacllem 49320 |
| Copyright terms: Public domain | W3C validator |