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 251 | . 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂)) | |
3 | 3anbi12d.2 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
4 | 1, 2, 3 | 3anbi123d 1391 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜂 ∧ 𝜃) ↔ (𝜒 ∧ 𝜂 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: 3anbi3d 1397 ax12wdemo 1999 f1dom3el3dif 6426 wfrlem1 7301 wfrlem3a 7304 wfrlem15 7316 cofsmo 8974 axdc3lem3 9157 axdc3lem4 9158 iscatd2 16165 psgnunilem1 17736 nn0gsumfz 18203 opprsubrg 18624 lsspropd 18838 mdetunilem3 20239 mdetunilem9 20245 smadiadetr 20300 lmres 20914 cnhaus 20968 regsep2 20990 dishaus 20996 ordthauslem 20997 nconsubb 21036 pthaus 21251 txhaus 21260 xkohaus 21266 regr1lem 21352 ustval 21816 methaus 22135 metnrmlem3 22472 pmltpclem1 23024 axtgeucl 25171 iscgrad 25503 dfcgra2 25521 f1otrge 25552 axeuclidlem 25642 2wlkonot 26392 2spthonot 26393 usg2spthonot0 26416 vdn0frgrav2 26550 vdgn0frgrav2 26551 vdn1frgrav2 26552 vdgn1frgrav2 26553 ex-opab 26681 isnvlem 26849 ajval 27101 adjeu 28132 adjval 28133 adj1 28176 adjeq 28178 cnlnssadj 28323 br8d 28802 lt2addrd 28903 xlt2addrd 28913 measval 29588 br8 30899 br6 30900 br4 30901 nofulllem5 31105 brcgr3 31323 brsegle 31385 fvray 31418 linedegen 31420 fvline 31421 poimirlem28 32607 isopos 33485 hlsuprexch 33685 2llnjN 33871 2lplnj 33924 cdlemk42 35247 zindbi 36529 jm2.27 36593 stoweidlem43 38936 fourierdlem42 39042 umgrvad2edg 40440 elwspths2spth 41171 upgr3v3e3cycl 41347 upgr4cycl4dv4e 41352 vdgn1frgrv2 41466 |
Copyright terms: Public domain | W3C validator |