![]() |
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 33380 bnj976 33788 bnj543 33904 bnj594 33923 bnj917 33945 topdifinffinlem 36228 dath 38607 oeord2com 42061 ichexmpl1 46137 elfzolborelfzop1 47200 nnolog2flm1 47276 isthincd2 47658 |
Copyright terms: Public domain | W3C validator |