| 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 2039 cbvexdw 2337 cbvexd 2406 cbvrexdva 3210 raleq 3287 rexeqbidvvOLD 3301 cbvrexdva2 3313 rexeqf 3321 cbvexeqsetf 3453 dfsbcq2 3747 unineq 4241 iindif2 5029 reusv2 5345 rabxfrd 5359 opeqex 5445 eqbrrdv 5740 eqbrrdiv 5741 opelco2g 5814 opelcnvg 5827 ralrnmptw 7032 ralrnmpt 7034 fliftcnv 7252 eusvobj2 7345 br1steqg 7953 br2ndeqg 7954 ottpos 8176 smoiso 8292 ercnv 8653 ordiso2 9426 cantnfrescl 9591 cantnfp1lem3 9595 cantnflem1b 9601 cantnflem1 9604 cnfcom 9615 cnfcom3lem 9618 djulf1o 9827 djurf1o 9828 carden2 9902 cardeq0 10465 axpownd 10514 fpwwe2lem8 10551 fzen 13463 hasheq0 14289 incexc2 15764 divalglem4 16326 divalglem8 16330 divalgb 16334 sadadd 16397 sadass 16401 smuval2 16412 smumul 16423 isprm3 16613 vdwmc 16909 imasleval 17464 acsfn2 17588 invsym2 17689 yoniso 18210 pmtrfmvdn0 19360 dprd2d2 19944 cmpfi 23312 xkoinjcn 23591 tgpconncomp 24017 iscau3 25195 mbfimaopnlem 25573 ellimc3 25797 eldv 25816 eltayl 26284 atandm3 26805 noetasuplem4 27665 rmoxfrd 32456 opeldifid 32562 2ndpreima 32669 f1od2 32682 ordtconnlem1 33910 bnj1253 35003 usgrgt2cycl 35122 satfdm 35361 wl-dral1d 37524 wl-sb8eft 37544 wl-sb8et 37546 wl-equsb3 37549 wl-sb8eut 37571 wl-sb8eutv 37572 wl-issetft 37575 wl-ax11-lem8 37585 poimirlem2 37621 poimirlem16 37635 poimirlem18 37637 poimirlem21 37640 poimirlem22 37641 eqbrrdv2 38861 islpln5 39534 islvol5 39578 ntrneicls11 44083 radcnvrat 44307 trsbc 44534 iindif2f 45158 ichnreuop 47476 ichreuopeq 47477 pm5.32dav 48798 exp12bd 48800 reuxfr1dd 48811 aacllem 49806 |
| Copyright terms: Public domain | W3C validator |