![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3anbi12d | 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 |
---|---|
3anbi12d | ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜂))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3anbi12d.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 3anbi12d.2 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
3 | biidd 252 | . 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂)) | |
4 | 1, 2, 3 | 3anbi123d 1547 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜂))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ w3a 1071 |
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 383 df-3an 1073 |
This theorem is referenced by: 3anbi1d 1551 3anbi2d 1552 f1dom3el3dif 6668 fseq1m1p1 12618 dfrtrcl2 14006 imasdsval 16379 iscatd2 16545 ispos 17151 psgnunilem1 18116 ringpropd 18786 mdetunilem3 20634 mdetunilem9 20640 dvfsumlem2 24006 istrkge 25573 axtg5seg 25581 axtgeucl 25588 iscgrad 25920 axlowdim 26058 axeuclid 26060 eengtrkge 26083 umgrvad2edg 26323 upgr3v3e3cycl 27356 upgr4cycl4dv4e 27361 lt2addrd 29852 xlt2addrd 29859 sigaval 30509 issgon 30522 brafs 31086 etasslt 32253 brofs 32445 funtransport 32471 fvtransport 32472 brifs 32483 ifscgr 32484 brcgr3 32486 cgr3permute3 32487 brfs 32519 btwnconn1lem11 32537 funray 32580 fvray 32581 funline 32582 fvline 32584 lpolsetN 37289 rmydioph 38104 iunrelexpmin2 38527 |
Copyright terms: Public domain | W3C validator |