![]() |
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 3538 vtocl3ga 3539 offval22 8025 ereq2 8663 brttrcl 9658 ttrclss 9665 ttrclselem2 9671 wrdl3s3 14863 mhmlem 18881 isdrngrd 20256 isdrngrdOLD 20258 lmodlema 20383 mdetunilem9 22006 neiptoptop 22519 neiptopnei 22520 hausnei 22716 regr1lem2 23128 ustuqtop4 23633 utopsnneiplem 23636 axtg5seg 27470 axtgupdim2 27476 axtgeucl 27477 brbtwn 27911 axlowdim 27973 axeuclidlem 27974 incistruhgr 28093 issubgr2 28283 wwlksnwwlksnon 28923 upgr4cycl4dv4e 29192 isnvlem 29615 csmdsymi 31339 br8d 31596 slmdlema 32108 carsgmon 33003 sitgclg 33031 tgoldbachgt 33365 axtgupdim2ALTV 33370 bnj852 33622 bnj18eq1 33628 bnj938 33638 bnj983 33652 bnj1318 33726 bnj1326 33727 cvmlift3lem4 34003 cvmlift3 34009 br8 34415 br6 34416 br4 34417 brcolinear2 34719 colineardim1 34722 brfs 34740 fscgr 34741 btwnconn1lem7 34754 brsegle 34769 unblimceq0 35046 sdclem2 36274 sdclem1 36275 sdc 36276 fdc 36277 cdleme18d 38831 cdlemk35s 39473 cdlemk39s 39475 monotoddzz 41325 jm2.27 41390 mendlmod 41578 minregex2 41929 fiiuncl 43395 wessf1ornlem 43525 fmulcl 43942 fmuldfeqlem1 43943 fprodcncf 44261 dvmptfprodlem 44305 dvmptfprod 44306 dvnprodlem2 44308 stoweidlem6 44367 stoweidlem8 44369 stoweidlem31 44392 stoweidlem34 44395 stoweidlem43 44404 stoweidlem52 44413 fourierdlem41 44509 fourierdlem48 44515 fourierdlem49 44516 ovnsubaddlem1 44931 ichexmpl2 45782 9gbo 46086 11gbo 46087 lmod1 46693 |
Copyright terms: Public domain | W3C validator |