![]() |
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 252 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃)) | |
2 | 3anbi1d.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | 3anbi12d 1548 | 1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ w3a 1071 |
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 197 df-an 383 df-3an 1073 |
This theorem is referenced by: vtocl3gaf 3426 offval22 7403 ereq2 7903 wrdl3s3 13914 mhmlem 17742 isdrngrd 18982 lmodlema 19077 mdetunilem9 20643 neiptoptop 21155 neiptopnei 21156 hausnei 21352 regr1lem2 21763 ustuqtop4 22267 utopsnneiplem 22270 axtg5seg 25584 axtgupdim2 25590 axtgeucl 25591 brbtwn 25999 axlowdim 26061 axeuclidlem 26062 incistruhgr 26194 issubgr2 26386 wwlksnwwlksnon 27059 wwlksnwwlksnonOLD 27061 upgr4cycl4dv4e 27364 isnvlem 27802 csmdsymi 29530 br8d 29757 slmdlema 30093 carsgmon 30713 sitgclg 30741 tgoldbachgt 31078 axtgupdim2OLD 31083 bnj852 31326 bnj18eq1 31332 bnj938 31342 bnj983 31356 bnj1318 31428 bnj1326 31429 cvmlift3lem4 31639 cvmlift3 31645 br8 31981 br6 31982 br4 31983 brcolinear2 32499 colineardim1 32502 brfs 32520 fscgr 32521 btwnconn1lem7 32534 brsegle 32549 unblimceq0 32832 sdclem2 33866 sdclem1 33867 sdc 33868 fdc 33869 cdleme18d 36100 cdlemk35s 36742 cdlemk39s 36744 monotoddzz 38030 jm2.27 38097 mendlmod 38285 fiiuncl 39751 wessf1ornlem 39887 fmulcl 40327 fmuldfeqlem1 40328 fprodcncf 40628 dvmptfprodlem 40673 dvmptfprod 40674 dvnprodlem2 40676 stoweidlem6 40736 stoweidlem8 40738 stoweidlem31 40761 stoweidlem34 40764 stoweidlem43 40773 stoweidlem52 40782 fourierdlem41 40878 fourierdlem48 40884 fourierdlem49 40885 ovnsubaddlem1 41300 9gbo 42186 11gbo 42187 lmod1 42805 |
Copyright terms: Public domain | W3C validator |