![]() |
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 1437 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ w3a 1087 |
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 1089 |
This theorem is referenced by: vtocl3gaf 3537 vtocl3ga 3538 axdc4uz 13888 wrdl3s3 14850 relexpindlem 14947 sqrtval 15121 sqreu 15244 coprmprod 16536 mreexexd 17527 iscatd2 17560 lmodprop2d 20382 neiptopnei 22481 hausnei 22677 isreg2 22726 regr1lem2 23089 ustval 23552 ustuqtop4 23594 axtgupdim2 27411 axtgeucl 27412 iscgra 27749 brbtwn 27846 ax5seg 27885 axlowdim 27908 axeuclidlem 27909 wlkonprop 28604 upgr2wlk 28614 upgrf1istrl 28649 elwspths2spth 28910 clwlkclwwlk 28944 clwwlknonel 29037 upgr4cycl4dv4e 29127 extwwlkfab 29294 nvi 29554 br8d 31527 xlt2addrd 31658 isslmd 32032 slmdlema 32033 tgoldbachgt 33267 axtgupdim2ALTV 33272 br8 34320 br6 34321 br4 34322 fvtransport 34608 brcolinear2 34634 colineardim1 34637 fscgr 34656 idinside 34660 brsegle 34684 poimirlem28 36097 caures 36210 iscringd 36448 oposlem 37635 cdleme18d 38749 jm2.27 41310 ichexmpl2 45634 ichnreuop 45636 9gbo 45938 11gbo 45939 |
Copyright terms: Public domain | W3C validator |