![]() |
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 262 | . 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂)) | |
4 | 1, 2, 3 | 3anbi123d 1432 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜂))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ w3a 1084 |
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 396 df-3an 1086 |
This theorem is referenced by: 3anbi1d 1436 3anbi2d 1437 f1dom3el3dif 7260 xpord2pred 8125 fseq1m1p1 13573 dfrtrcl2 15006 imasdsval 17460 iscatd2 17624 ispos 18269 psgnunilem1 19403 rngpropd 20069 ringpropd 20177 mdetunilem3 22438 mdetunilem9 22444 dvfsumlem2 25883 dvfsumlem2OLD 25884 istrkge 28177 axtg5seg 28185 axtgeucl 28192 iscgrad 28531 axlowdim 28688 axeuclid 28690 eengtrkge 28714 umgrvad2edg 28939 upgr3v3e3cycl 29902 upgr4cycl4dv4e 29907 lt2addrd 32433 xlt2addrd 32440 sigaval 33598 issgon 33610 brafs 34173 loop1cycl 34617 brofs 35472 funtransport 35498 fvtransport 35499 brifs 35510 ifscgr 35511 brcgr3 35513 cgr3permute3 35514 brfs 35546 btwnconn1lem11 35564 funray 35607 fvray 35608 funline 35609 fvline 35611 lpolsetN 40843 rmydioph 42242 tfsconcatrev 42587 iunrelexpmin2 42952 fundcmpsurinj 46562 ichexmpl1 46622 iscnrm3r 47769 iscnrm3l 47772 |
Copyright terms: Public domain | W3C validator |