![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3anbi2d | Structured version Visualization version GIF version |
Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.) |
Ref | Expression |
---|---|
3anbi1d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
3anbi2d | ⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biidd 261 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃)) | |
2 | 3anbi1d.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | 3anbi12d 1437 | 1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ w3a 1087 |
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 df-an 397 df-3an 1089 |
This theorem is referenced by: vtocl3gaf 3535 vtocl3ga 3536 offval22 8012 ereq2 8614 brttrcl 9607 ttrclss 9614 ttrclselem2 9620 wrdl3s3 14811 mhmlem 18826 isdrngrd 20168 lmodlema 20280 mdetunilem9 21921 neiptoptop 22434 neiptopnei 22435 hausnei 22631 regr1lem2 23043 ustuqtop4 23548 utopsnneiplem 23551 axtg5seg 27236 axtgupdim2 27242 axtgeucl 27243 brbtwn 27677 axlowdim 27739 axeuclidlem 27740 incistruhgr 27859 issubgr2 28049 wwlksnwwlksnon 28689 upgr4cycl4dv4e 28958 isnvlem 29381 csmdsymi 31105 br8d 31358 slmdlema 31864 carsgmon 32726 sitgclg 32754 tgoldbachgt 33088 axtgupdim2ALTV 33093 bnj852 33345 bnj18eq1 33351 bnj938 33361 bnj983 33375 bnj1318 33449 bnj1326 33450 cvmlift3lem4 33728 cvmlift3 33734 br8 34145 br6 34146 br4 34147 brcolinear2 34581 colineardim1 34584 brfs 34602 fscgr 34603 btwnconn1lem7 34616 brsegle 34631 unblimceq0 34908 sdclem2 36139 sdclem1 36140 sdc 36141 fdc 36142 cdleme18d 38696 cdlemk35s 39338 cdlemk39s 39340 monotoddzz 41176 jm2.27 41241 mendlmod 41429 minregex2 41718 fiiuncl 43184 wessf1ornlem 43308 fmulcl 43723 fmuldfeqlem1 43724 fprodcncf 44042 dvmptfprodlem 44086 dvmptfprod 44087 dvnprodlem2 44089 stoweidlem6 44148 stoweidlem8 44150 stoweidlem31 44173 stoweidlem34 44176 stoweidlem43 44185 stoweidlem52 44194 fourierdlem41 44290 fourierdlem48 44296 fourierdlem49 44297 ovnsubaddlem1 44712 ichexmpl2 45563 9gbo 45867 11gbo 45868 lmod1 46474 |
Copyright terms: Public domain | W3C validator |