![]() |
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 290. 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 274 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒)) |
4 | 3bitr3g.3 | . 2 ⊢ (𝜒 ↔ 𝜏) | |
5 | 3, 4 | syl6bb 276 | 1 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 |
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 197 |
This theorem is referenced by: notbid 307 cador 1587 cbvexdva 2319 dfsbcq2 3471 unineq 3910 iindif2 4621 reusv2 4904 rabxfrd 4919 opeqex 4991 eqbrrdv 5251 eqbrrdiv 5252 opelco2g 5322 opelcnvg 5334 ralrnmpt 6408 fliftcnv 6601 eusvobj2 6683 br1steqg 7232 br2ndeqg 7233 ottpos 7407 smoiso 7504 ercnv 7808 ordiso2 8461 cantnfrescl 8611 cantnfp1lem3 8615 cantnflem1b 8621 cantnflem1 8624 cnfcom 8635 cnfcom3lem 8638 carden2 8851 cardeq0 9412 axpownd 9461 fpwwe2lem9 9498 fzen 12396 hasheq0 13192 incexc2 14614 divalglem4 15166 divalglem8 15170 divalgb 15174 divalgmodOLD 15177 sadadd 15236 sadass 15240 smuval2 15251 smumul 15262 isprm3 15443 vdwmc 15729 imasleval 16248 acsfn2 16371 invsym2 16470 yoniso 16972 pmtrfmvdn0 17928 dprd2d2 18489 cmpfi 21259 xkoinjcn 21538 tgpconncomp 21963 iscau3 23122 mbfimaopnlem 23467 ellimc3 23688 eldv 23707 eltayl 24159 atandm3 24650 rmoxfrdOLD 29459 rmoxfrd 29460 opeldifid 29538 2ndpreima 29613 f1od2 29627 ordtconnlem1 30098 bnj1253 31211 noetalem3 31990 wl-dral1d 33448 wl-sb8et 33464 wl-equsb3 33467 wl-sb8eut 33489 wl-ax11-lem8 33499 poimirlem2 33541 poimirlem16 33555 poimirlem18 33557 poimirlem21 33560 poimirlem22 33561 eqbrrdv2 34467 islpln5 35139 islvol5 35183 ntrneicls11 38705 radcnvrat 38830 trsbc 39067 aacllem 42875 |
Copyright terms: Public domain | W3C validator |