![]() |
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 261 | . 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂)) | |
3 | 3anbi12d.2 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
4 | 1, 2, 3 | 3anbi123d 1436 | 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: 3anbi3d 1442 ax12wdemo 2131 f1dom3el3dif 7213 xpord2lem 8071 xpord3lem 8078 frrlem1 8214 frrlem13 8226 wfrlem1OLD 8251 wfrlem3OLDa 8254 wfrlem15OLD 8266 cofsmo 10202 axdc3lem3 10385 axdc3lem4 10386 iscatd2 17558 psgnunilem1 19271 nn0gsumfz 19757 opprsubrg 20239 lsspropd 20474 mdetunilem3 21959 mdetunilem9 21965 smadiadetr 22020 lmres 22647 cnhaus 22701 regsep2 22723 dishaus 22729 ordthauslem 22730 nconnsubb 22770 pthaus 22985 txhaus 22994 xkohaus 23000 regr1lem 23086 ustval 23550 methaus 23872 metnrmlem3 24220 pmltpclem1 24808 brsslt 27121 axtgeucl 27312 iscgrad 27651 dfcgra2 27670 f1otrge 27712 axeuclidlem 27809 umgrvad2edg 28059 elwspths2spth 28810 upgr3v3e3cycl 29022 upgr4cycl4dv4e 29027 vdgn1frgrv2 29138 numclwlk1lem1 29211 ex-opab 29274 isnvlem 29450 ajval 29701 adjeu 30729 adjval 30730 adj1 30773 adjeq 30775 cnlnssadj 30920 br8d 31427 lt2addrd 31551 xlt2addrd 31558 measval 32688 loop1cycl 33622 br8 34221 br6 34222 br4 34223 brcgr3 34620 brsegle 34682 fvray 34715 linedegen 34717 fvline 34718 poimirlem28 36095 isopos 37631 hlsuprexch 37833 2llnjN 38019 2lplnj 38072 cdlemk42 39393 zindbi 41246 jm2.27 41308 nnoeomeqom 41622 rp-brsslt 41675 stoweidlem43 44254 fourierdlem42 44360 ichexmpl1 45631 sepfsepc 46930 iscnrm3rlem8 46950 iscnrm3llem2 46953 |
Copyright terms: Public domain | W3C validator |