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 265 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃)) | |
2 | 3anbi1d.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | 3anbi12d 1439 | 1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: vtocl3gaf 3489 vtocl3ga 3490 offval22 7853 ereq2 8396 wrdl3s3 14526 mhmlem 18480 isdrngrd 19790 lmodlema 19901 mdetunilem9 21514 neiptoptop 22025 neiptopnei 22026 hausnei 22222 regr1lem2 22634 ustuqtop4 23139 utopsnneiplem 23142 axtg5seg 26553 axtgupdim2 26559 axtgeucl 26560 brbtwn 26987 axlowdim 27049 axeuclidlem 27050 incistruhgr 27167 issubgr2 27357 wwlksnwwlksnon 27996 upgr4cycl4dv4e 28265 isnvlem 28688 csmdsymi 30412 br8d 30666 slmdlema 31172 carsgmon 31990 sitgclg 32018 tgoldbachgt 32352 axtgupdim2ALTV 32357 bnj852 32611 bnj18eq1 32617 bnj938 32627 bnj983 32641 bnj1318 32715 bnj1326 32716 cvmlift3lem4 32994 cvmlift3 33000 br8 33439 br6 33440 br4 33441 brttrcl 33509 ttrclss 33516 brcolinear2 34094 colineardim1 34097 brfs 34115 fscgr 34116 btwnconn1lem7 34129 brsegle 34144 unblimceq0 34421 sdclem2 35635 sdclem1 35636 sdc 35637 fdc 35638 cdleme18d 38044 cdlemk35s 38686 cdlemk39s 38688 monotoddzz 40466 jm2.27 40531 mendlmod 40719 fiiuncl 42284 wessf1ornlem 42393 fmulcl 42795 fmuldfeqlem1 42796 fprodcncf 43114 dvmptfprodlem 43158 dvmptfprod 43159 dvnprodlem2 43161 stoweidlem6 43220 stoweidlem8 43222 stoweidlem31 43245 stoweidlem34 43248 stoweidlem43 43257 stoweidlem52 43266 fourierdlem41 43362 fourierdlem48 43368 fourierdlem49 43369 ovnsubaddlem1 43781 ichexmpl2 44593 9gbo 44897 11gbo 44898 lmod1 45504 |
Copyright terms: Public domain | W3C validator |