![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3anbi13d | Structured version Visualization version GIF version |
Description: Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.) |
Ref | Expression |
---|---|
3anbi12d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
3anbi12d.2 | ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Ref | Expression |
---|---|
3anbi13d | ⊢ (𝜑 → ((𝜓 ∧ 𝜂 ∧ 𝜃) ↔ (𝜒 ∧ 𝜂 ∧ 𝜏))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3anbi12d.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | biidd 252 | . 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂)) | |
3 | 3anbi12d.2 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
4 | 1, 2, 3 | 3anbi123d 1439 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜂 ∧ 𝜃) ↔ (𝜒 ∧ 𝜂 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ w3a 1054 |
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 197 df-an 385 df-3an 1056 |
This theorem is referenced by: 3anbi3d 1445 ax12wdemo 2052 f1dom3el3dif 6566 wfrlem1 7459 wfrlem3a 7462 wfrlem15 7474 cofsmo 9129 axdc3lem3 9312 axdc3lem4 9313 iscatd2 16389 psgnunilem1 17959 nn0gsumfz 18426 opprsubrg 18849 lsspropd 19065 mdetunilem3 20468 mdetunilem9 20474 smadiadetr 20529 lmres 21152 cnhaus 21206 regsep2 21228 dishaus 21234 ordthauslem 21235 nconnsubb 21274 pthaus 21489 txhaus 21498 xkohaus 21504 regr1lem 21590 ustval 22053 methaus 22372 metnrmlem3 22711 pmltpclem1 23263 axtgeucl 25416 iscgrad 25748 dfcgra2 25766 f1otrge 25797 axeuclidlem 25887 umgrvad2edg 26150 elwspths2spth 26934 upgr3v3e3cycl 27158 upgr4cycl4dv4e 27163 vdgn1frgrv2 27276 ex-opab 27419 isnvlem 27593 ajval 27845 adjeu 28876 adjval 28877 adj1 28920 adjeq 28922 cnlnssadj 29067 br8d 29548 lt2addrd 29644 xlt2addrd 29651 measval 30389 br8 31772 br6 31773 br4 31774 frrlem1 31905 brsslt 32025 brcgr3 32278 brsegle 32340 fvray 32373 linedegen 32375 fvline 32376 poimirlem28 33567 isopos 34785 hlsuprexch 34985 2llnjN 35171 2lplnj 35224 cdlemk42 36546 zindbi 37828 jm2.27 37892 stoweidlem43 40578 fourierdlem42 40684 |
Copyright terms: Public domain | W3C validator |