![]() |
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 262 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃)) | |
2 | 3anbi1d.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | 3anbi12d 1438 | 1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: vtocl3gaf 3536 vtocl3ga 3537 offval22 8021 ereq2 8659 brttrcl 9654 ttrclss 9661 ttrclselem2 9667 wrdl3s3 14857 mhmlem 18872 isdrngrd 20227 isdrngrdOLD 20229 lmodlema 20341 mdetunilem9 21985 neiptoptop 22498 neiptopnei 22499 hausnei 22695 regr1lem2 23107 ustuqtop4 23612 utopsnneiplem 23615 axtg5seg 27449 axtgupdim2 27455 axtgeucl 27456 brbtwn 27890 axlowdim 27952 axeuclidlem 27953 incistruhgr 28072 issubgr2 28262 wwlksnwwlksnon 28902 upgr4cycl4dv4e 29171 isnvlem 29594 csmdsymi 31318 br8d 31575 slmdlema 32087 carsgmon 32971 sitgclg 32999 tgoldbachgt 33333 axtgupdim2ALTV 33338 bnj852 33590 bnj18eq1 33596 bnj938 33606 bnj983 33620 bnj1318 33694 bnj1326 33695 cvmlift3lem4 33973 cvmlift3 33979 br8 34385 br6 34386 br4 34387 brcolinear2 34689 colineardim1 34692 brfs 34710 fscgr 34711 btwnconn1lem7 34724 brsegle 34739 unblimceq0 35016 sdclem2 36247 sdclem1 36248 sdc 36249 fdc 36250 cdleme18d 38804 cdlemk35s 39446 cdlemk39s 39448 monotoddzz 41310 jm2.27 41375 mendlmod 41563 minregex2 41895 fiiuncl 43361 wessf1ornlem 43491 fmulcl 43908 fmuldfeqlem1 43909 fprodcncf 44227 dvmptfprodlem 44271 dvmptfprod 44272 dvnprodlem2 44274 stoweidlem6 44333 stoweidlem8 44335 stoweidlem31 44358 stoweidlem34 44361 stoweidlem43 44370 stoweidlem52 44379 fourierdlem41 44475 fourierdlem48 44481 fourierdlem49 44482 ovnsubaddlem1 44897 ichexmpl2 45748 9gbo 46052 11gbo 46053 lmod1 46659 |
Copyright terms: Public domain | W3C validator |