![]() |
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 293. 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 | syl5bbr 277 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒)) |
4 | 3bitr3g.3 | . 2 ⊢ (𝜒 ↔ 𝜏) | |
5 | 3, 4 | syl6bb 279 | 1 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 |
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 199 |
This theorem is referenced by: notbid 310 cador 1666 cbvexd 2373 cbvexdva 2377 dfsbcq2 3655 unineq 4104 iindif2 4824 reusv2 5117 rabxfrd 5131 opeqex 5195 eqbrrdv 5466 eqbrrdiv 5467 opelco2g 5537 opelcnvg 5550 ralrnmpt 6634 fliftcnv 6835 eusvobj2 6917 br1steqg 7469 br2ndeqg 7470 ottpos 7646 smoiso 7744 ercnv 8049 ordiso2 8711 cantnfrescl 8872 cantnfp1lem3 8876 cantnflem1b 8882 cantnflem1 8885 cnfcom 8896 cnfcom3lem 8899 djulf1o 9073 djurf1o 9074 carden2 9148 cardeq0 9711 axpownd 9760 fpwwe2lem9 9797 fzen 12680 hasheq0 13475 incexc2 14983 divalglem4 15536 divalglem8 15540 divalgb 15544 sadadd 15605 sadass 15609 smuval2 15620 smumul 15631 isprm3 15812 vdwmc 16097 imasleval 16598 acsfn2 16720 invsym2 16819 yoniso 17322 pmtrfmvdn0 18276 dprd2d2 18841 cmpfi 21631 xkoinjcn 21910 tgpconncomp 22335 iscau3 23495 mbfimaopnlem 23870 ellimc3 24091 eldv 24110 eltayl 24562 atandm3 25067 rmoxfrd 29916 opeldifid 29992 2ndpreima 30068 f1od2 30082 ordtconnlem1 30576 bnj1253 31692 noetalem3 32462 wl-dral1d 33919 wl-sb8et 33936 wl-equsb3 33939 wl-sb8eut 33960 wl-ax11-lem8 33970 wl-clelsb3df 34005 poimirlem2 34046 poimirlem16 34060 poimirlem18 34062 poimirlem21 34065 poimirlem22 34066 eqbrrdv2 35026 islpln5 35698 islvol5 35742 ntrneicls11 39358 radcnvrat 39483 trsbc 39714 aacllem 43667 |
Copyright terms: Public domain | W3C validator |