| 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 262 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃)) | |
| 3 | 1, 2 | 3anbi12d 1439 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: vtocl3gafOLD 3582 vtocl3gaOLD 3584 axdc4uz 14025 wrdl3s3 15001 relexpindlem 15102 sqrtval 15276 sqreu 15399 coprmprod 16698 mreexexd 17691 iscatd2 17724 lmodprop2d 20922 neiptopnei 23140 hausnei 23336 isreg2 23385 regr1lem2 23748 ustval 24211 ustuqtop4 24253 axtgupdim2 28479 axtgeucl 28480 iscgra 28817 brbtwn 28914 ax5seg 28953 axlowdim 28976 axeuclidlem 28977 wlkonprop 29676 upgr2wlk 29686 upgrf1istrl 29721 elwspths2spth 29987 clwlkclwwlk 30021 clwwlknonel 30114 upgr4cycl4dv4e 30204 extwwlkfab 30371 nvi 30633 br8d 32622 xlt2addrd 32762 isslmd 33208 slmdlema 33209 tgoldbachgt 34678 axtgupdim2ALTV 34683 br8 35756 br6 35757 br4 35758 fvtransport 36033 brcolinear2 36059 colineardim1 36062 fscgr 36081 idinside 36085 brsegle 36109 poimirlem28 37655 caures 37767 iscringd 38005 oposlem 39183 cdleme18d 40297 jm2.27 43020 ichexmpl2 47457 ichnreuop 47459 9gbo 47761 11gbo 47762 |
| Copyright terms: Public domain | W3C validator |