![]() |
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 263 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃)) | |
2 | 3anbi1d.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | 3anbi12d 1429 | 1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ w3a 1080 |
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 208 df-an 397 df-3an 1082 |
This theorem is referenced by: vtocl3gaf 3520 offval22 7644 ereq2 8152 wrdl3s3 14165 mhmlem 17981 isdrngrd 19223 lmodlema 19334 mdetunilem9 20918 neiptoptop 21428 neiptopnei 21429 hausnei 21625 regr1lem2 22037 ustuqtop4 22541 utopsnneiplem 22544 axtg5seg 25938 axtgupdim2 25944 axtgeucl 25945 brbtwn 26373 axlowdim 26435 axeuclidlem 26436 incistruhgr 26552 issubgr2 26742 wwlksnwwlksnon 27386 upgr4cycl4dv4e 27656 isnvlem 28083 csmdsymi 29807 br8d 30056 slmdlema 30474 carsgmon 31194 sitgclg 31222 tgoldbachgt 31556 axtgupdim2ALTV 31561 bnj852 31814 bnj18eq1 31820 bnj938 31830 bnj983 31844 bnj1318 31916 bnj1326 31917 cvmlift3lem4 32184 cvmlift3 32190 br8 32607 br6 32608 br4 32609 brcolinear2 33135 colineardim1 33138 brfs 33156 fscgr 33157 btwnconn1lem7 33170 brsegle 33185 unblimceq0 33462 sdclem2 34575 sdclem1 34576 sdc 34577 fdc 34578 cdleme18d 36988 cdlemk35s 37630 cdlemk39s 37632 monotoddzz 39051 jm2.27 39116 mendlmod 39304 fiiuncl 40892 wessf1ornlem 41011 fmulcl 41430 fmuldfeqlem1 41431 fprodcncf 41752 dvmptfprodlem 41797 dvmptfprod 41798 dvnprodlem2 41800 stoweidlem6 41860 stoweidlem8 41862 stoweidlem31 41885 stoweidlem34 41888 stoweidlem43 41897 stoweidlem52 41906 fourierdlem41 42002 fourierdlem48 42008 fourierdlem49 42009 ovnsubaddlem1 42421 ichexmpl2 43141 9gbo 43448 11gbo 43449 lmod1 44054 |
Copyright terms: Public domain | W3C validator |