![]() |
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 1434 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: vtocl3gafOLD 3563 vtocl3gaOLD 3565 axdc4uz 14004 wrdl3s3 14971 relexpindlem 15068 sqrtval 15242 sqreu 15365 coprmprod 16662 mreexexd 17661 iscatd2 17694 lmodprop2d 20900 neiptopnei 23127 hausnei 23323 isreg2 23372 regr1lem2 23735 ustval 24198 ustuqtop4 24240 axtgupdim2 28398 axtgeucl 28399 iscgra 28736 brbtwn 28833 ax5seg 28872 axlowdim 28895 axeuclidlem 28896 wlkonprop 29595 upgr2wlk 29605 upgrf1istrl 29640 elwspths2spth 29901 clwlkclwwlk 29935 clwwlknonel 30028 upgr4cycl4dv4e 30118 extwwlkfab 30285 nvi 30547 br8d 32530 xlt2addrd 32662 isslmd 33066 slmdlema 33067 tgoldbachgt 34509 axtgupdim2ALTV 34514 br8 35578 br6 35579 br4 35580 fvtransport 35856 brcolinear2 35882 colineardim1 35885 fscgr 35904 idinside 35908 brsegle 35932 poimirlem28 37349 caures 37461 iscringd 37699 oposlem 38880 cdleme18d 39994 jm2.27 42666 ichexmpl2 47042 ichnreuop 47044 9gbo 47346 11gbo 47347 |
Copyright terms: Public domain | W3C validator |