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 265 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃)) | |
3 | 1, 2 | 3anbi12d 1438 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ w3a 1088 |
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 1090 |
This theorem is referenced by: vtocl3gaf 3480 axdc4uz 13436 wrdl3s3 14408 relexpindlem 14505 sqrtval 14679 sqreu 14803 coprmprod 16095 mreexexd 17015 iscatd2 17048 lmodprop2d 19808 neiptopnei 21876 hausnei 22072 isreg2 22121 regr1lem2 22484 ustval 22947 ustuqtop4 22989 axtgupdim2 26409 axtgeucl 26410 iscgra 26747 brbtwn 26837 ax5seg 26876 axlowdim 26899 axeuclidlem 26900 wlkonprop 27592 upgr2wlk 27602 upgrf1istrl 27637 elwspths2spth 27897 clwlkclwwlk 27931 clwwlknonel 28024 upgr4cycl4dv4e 28114 extwwlkfab 28281 nvi 28541 br8d 30516 xlt2addrd 30648 isslmd 31024 slmdlema 31025 tgoldbachgt 32205 axtgupdim2ALTV 32210 br8 33287 br6 33288 br4 33289 fvtransport 33964 brcolinear2 33990 colineardim1 33993 fscgr 34012 idinside 34016 brsegle 34040 poimirlem28 35417 caures 35530 iscringd 35768 oposlem 36808 cdleme18d 37921 jm2.27 40386 ichexmpl2 44440 ichnreuop 44442 9gbo 44744 11gbo 44745 |
Copyright terms: Public domain | W3C validator |