![]() |
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 254 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃)) | |
3 | 1, 2 | 3anbi12d 1567 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ w3a 1113 |
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 199 df-an 387 df-3an 1115 |
This theorem is referenced by: vtocl3gaf 3491 axdc4uz 13077 wrdl3s3 14083 relexpindlem 14179 sqrtval 14353 sqreu 14476 coprmprod 15746 mreexexd 16660 iscatd2 16693 lmodprop2d 19280 neiptopnei 21306 hausnei 21502 isreg2 21551 regr1lem2 21913 ustval 22375 ustuqtop4 22417 axtgupdim2 25782 axtgeucl 25783 iscgra 26117 brbtwn 26197 ax5seg 26236 axlowdim 26259 axeuclidlem 26260 wlkonprop 26954 upgr2wlk 26964 upgrf1istrl 27005 elwspths2spth 27295 clwlkclwwlk 27330 clwlkclwwlkOLD 27331 clwwlknonel 27467 upgr4cycl4dv4e 27560 extwwlkfab 27739 extwwlkfabOLD 27740 nvi 28023 br8d 29968 xlt2addrd 30069 isslmd 30299 slmdlema 30300 tgoldbachgt 31289 axtgupdim2OLD 31294 br8 32187 br6 32188 br4 32189 fvtransport 32677 brcolinear2 32703 colineardim1 32706 fscgr 32725 idinside 32729 brsegle 32753 poimirlem28 33980 caures 34097 iscringd 34338 oposlem 35256 cdleme18d 36369 jm2.27 38417 9gbo 42491 11gbo 42492 |
Copyright terms: Public domain | W3C validator |