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 263 | . 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂)) | |
4 | 1, 2, 3 | 3anbi123d 1427 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜂))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: 3anbi1d 1431 3anbi2d 1432 f1dom3el3dif 7018 fseq1m1p1 12970 dfrtrcl2 14409 imasdsval 16776 iscatd2 16940 ispos 17545 psgnunilem1 18550 ringpropd 19261 mdetunilem3 21151 mdetunilem9 21157 dvfsumlem2 24551 istrkge 26170 axtg5seg 26178 axtgeucl 26185 iscgrad 26524 axlowdim 26674 axeuclid 26676 eengtrkge 26700 umgrvad2edg 26922 upgr3v3e3cycl 27886 upgr4cycl4dv4e 27891 lt2addrd 30401 xlt2addrd 30408 sigaval 31269 issgon 31281 brafs 31842 loop1cycl 32281 etasslt 33171 brofs 33363 funtransport 33389 fvtransport 33390 brifs 33401 ifscgr 33402 brcgr3 33404 cgr3permute3 33405 brfs 33437 btwnconn1lem11 33455 funray 33498 fvray 33499 funline 33500 fvline 33502 lpolsetN 38498 rmydioph 39489 iunrelexpmin2 39935 fundcmpsurinj 43446 ichexmpl1 43508 |
Copyright terms: Public domain | W3C validator |