![]() |
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 261 | . 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂)) | |
4 | 1, 2, 3 | 3anbi123d 1436 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜂))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ 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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: 3anbi1d 1440 3anbi2d 1441 f1dom3el3dif 7221 xpord2pred 8082 fseq1m1p1 13526 dfrtrcl2 14959 imasdsval 17411 iscatd2 17575 ispos 18217 psgnunilem1 19289 ringpropd 20020 mdetunilem3 22000 mdetunilem9 22006 dvfsumlem2 25428 istrkge 27462 axtg5seg 27470 axtgeucl 27477 iscgrad 27816 axlowdim 27973 axeuclid 27975 eengtrkge 27999 umgrvad2edg 28224 upgr3v3e3cycl 29187 upgr4cycl4dv4e 29192 lt2addrd 31724 xlt2addrd 31731 sigaval 32799 issgon 32811 brafs 33374 loop1cycl 33818 brofs 34666 funtransport 34692 fvtransport 34693 brifs 34704 ifscgr 34705 brcgr3 34707 cgr3permute3 34708 brfs 34740 btwnconn1lem11 34758 funray 34801 fvray 34802 funline 34803 fvline 34805 lpolsetN 40018 rmydioph 41396 tfsconcatrev 41741 iunrelexpmin2 42106 fundcmpsurinj 45721 ichexmpl1 45781 iscnrm3r 47101 iscnrm3l 47104 |
Copyright terms: Public domain | W3C validator |