Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3anbi1d | 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 |
---|---|
3anbi1d | ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3anbi1d.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | biidd 261 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃)) | |
3 | 1, 2 | 3anbi12d 1436 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ w3a 1086 |
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 1088 |
This theorem is referenced by: vtocl3gaf 3517 vtocl3ga 3518 axdc4uz 13713 wrdl3s3 14686 relexpindlem 14783 sqrtval 14957 sqreu 15081 coprmprod 16375 mreexexd 17366 iscatd2 17399 lmodprop2d 20194 neiptopnei 22292 hausnei 22488 isreg2 22537 regr1lem2 22900 ustval 23363 ustuqtop4 23405 axtgupdim2 26841 axtgeucl 26842 iscgra 27179 brbtwn 27276 ax5seg 27315 axlowdim 27338 axeuclidlem 27339 wlkonprop 28035 upgr2wlk 28045 upgrf1istrl 28080 elwspths2spth 28341 clwlkclwwlk 28375 clwwlknonel 28468 upgr4cycl4dv4e 28558 extwwlkfab 28725 nvi 28985 br8d 30959 xlt2addrd 31090 isslmd 31464 slmdlema 31465 tgoldbachgt 32652 axtgupdim2ALTV 32657 br8 33732 br6 33733 br4 33734 fvtransport 34343 brcolinear2 34369 colineardim1 34372 fscgr 34391 idinside 34395 brsegle 34419 poimirlem28 35814 caures 35927 iscringd 36165 oposlem 37203 cdleme18d 38316 jm2.27 40837 ichexmpl2 44933 ichnreuop 44935 9gbo 45237 11gbo 45238 |
Copyright terms: Public domain | W3C validator |