| 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 1438 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜂))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ w3a 1087 |
| 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: 3anbi1d 1442 3anbi2d 1443 f1dom3el3dif 7289 xpord2pred 8170 fseq1m1p1 13639 dfrtrcl2 15101 imasdsval 17560 iscatd2 17724 ispos 18360 psgnunilem1 19511 rngpropd 20171 ringpropd 20285 mdetunilem3 22620 mdetunilem9 22626 dvfsumlem2 26067 dvfsumlem2OLD 26068 istrkge 28465 axtg5seg 28473 axtgeucl 28480 iscgrad 28819 axlowdim 28976 axeuclid 28978 eengtrkge 29002 umgrvad2edg 29230 upgr3v3e3cycl 30199 upgr4cycl4dv4e 30204 lt2addrd 32755 xlt2addrd 32762 constrsuc 33779 constrconj 33786 sigaval 34112 issgon 34124 brafs 34687 loop1cycl 35142 brofs 36006 funtransport 36032 fvtransport 36033 brifs 36044 ifscgr 36045 brcgr3 36047 cgr3permute3 36048 brfs 36080 btwnconn1lem11 36098 funray 36141 fvray 36142 funline 36143 fvline 36145 lpolsetN 41484 rmydioph 43026 tfsconcatrev 43361 iunrelexpmin2 43725 fundcmpsurinj 47396 ichexmpl1 47456 cycl3grtri 47914 grimgrtri 47916 usgrgrtrirex 47917 isubgr3stgrlem4 47936 grlimgrtri 47963 iscnrm3r 48845 iscnrm3l 48848 |
| Copyright terms: Public domain | W3C validator |