|   | 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 1155 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∧ w3a 1086 | 
| 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 1088 | 
| This theorem is referenced by: iinfi 9458 fzolb 13706 brfi1uzind 14548 opfi1uzind 14551 01sqrexlem5 15286 bitsmod 16474 isfunc 17910 txcn 23635 trfil2 23896 isclmp 25131 eulerpartlemn 34384 bnj976 34792 bnj543 34908 bnj594 34927 bnj917 34949 topdifinffinlem 37349 dath 39739 oeord2com 43329 ichexmpl1 47461 grtriproplem 47911 grtrif1o 47914 elfzolborelfzop1 48441 nnolog2flm1 48516 isthincd2 49111 | 
| Copyright terms: Public domain | W3C validator |