![]() |
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 1428 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜂))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ w3a 1080 |
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 1082 |
This theorem is referenced by: 3anbi1d 1432 3anbi2d 1433 f1dom3el3dif 6892 fseq1m1p1 12832 dfrtrcl2 14255 imasdsval 16617 iscatd2 16781 ispos 17386 psgnunilem1 18352 ringpropd 19022 mdetunilem3 20907 mdetunilem9 20913 dvfsumlem2 24307 istrkge 25925 axtg5seg 25933 axtgeucl 25940 iscgrad 26279 axlowdim 26430 axeuclid 26432 eengtrkge 26456 umgrvad2edg 26678 upgr3v3e3cycl 27646 upgr4cycl4dv4e 27651 lt2addrd 30163 xlt2addrd 30170 sigaval 30987 issgon 30999 brafs 31560 loop1cycl 31992 etasslt 32883 brofs 33075 funtransport 33101 fvtransport 33102 brifs 33113 ifscgr 33114 brcgr3 33116 cgr3permute3 33117 brfs 33149 btwnconn1lem11 33167 funray 33210 fvray 33211 funline 33212 fvline 33214 lpolsetN 38149 rmydioph 39096 iunrelexpmin2 39542 ichexmpl1 43113 |
Copyright terms: Public domain | W3C validator |