![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3anbi1i | Structured version Visualization version GIF version |
Description: Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.) |
Ref | Expression |
---|---|
3anbi1i.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
3anbi1i | ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3anbi1i.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
2 | biid 261 | . 2 ⊢ (𝜒 ↔ 𝜒) | |
3 | biid 261 | . 2 ⊢ (𝜃 ↔ 𝜃) | |
4 | 1, 2, 3 | 3anbi123i 1156 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: iinfi 9412 fzolb 13638 brfi1uzind 14459 opfi1uzind 14462 01sqrexlem5 15193 bitsmod 16377 isfunc 17814 txcn 23130 trfil2 23391 isclmp 24613 eulerpartlemn 33411 bnj976 33819 bnj543 33935 bnj594 33954 bnj917 33976 topdifinffinlem 36276 dath 38655 oeord2com 42109 ichexmpl1 46185 elfzolborelfzop1 47248 nnolog2flm1 47324 isthincd2 47706 |
Copyright terms: Public domain | W3C validator |