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 252 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃)) | |
3 | 1, 2 | 3anbi12d 1400 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ w3a 1037 |
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 386 df-3an 1039 |
This theorem is referenced by: vtocl3gaf 3275 axdc4uz 12783 wrdl3s3 13705 relexpindlem 13803 sqrtval 13977 sqreu 14100 coprmprod 15375 mreexexd 16308 mreexexdOLD 16309 iscatd2 16342 lmodprop2d 18925 neiptopnei 20936 hausnei 21132 isreg2 21181 regr1lem2 21543 ustval 22006 ustuqtop4 22048 axtgupdim2 25370 axtgeucl 25371 iscgra 25701 brbtwn 25779 ax5seg 25818 axlowdim 25841 axeuclidlem 25842 wlkonprop 26554 upgr2wlk 26564 upgrf1istrl 26600 elwspths2spth 26862 clwlkclwwlk 26903 upgr4cycl4dv4e 27045 extwwlkfab 27223 nvi 27469 br8d 29422 xlt2addrd 29523 isslmd 29755 slmdlema 29756 tgoldbachgt 30741 axtgupdim2OLD 30746 br8 31646 br6 31647 br4 31648 fvtransport 32139 brcolinear2 32165 colineardim1 32168 fscgr 32187 idinside 32191 brsegle 32215 poimirlem28 33437 caures 33556 iscringd 33797 oposlem 34469 cdleme18d 35582 jm2.27 37575 9gbo 41662 11gbo 41663 |
Copyright terms: Public domain | W3C validator |