|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > 3anbi3i | 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 | 
|---|---|
| 3anbi3i | ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | biid 261 | . 2 ⊢ (𝜒 ↔ 𝜒) | |
| 2 | biid 261 | . 2 ⊢ (𝜃 ↔ 𝜃) | |
| 3 | 3anbi1i.1 | . 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: cadcomb 1612 dfwrecsOLD 8339 dfer2 8747 ttrclresv 9758 axgroth2 10866 oppgsubm 19382 xrsdsreclb 21432 ordthaus 23393 qtopeu 23725 regr1lem2 23749 isfbas2 23844 isclmp 25131 umgr2edg1 29229 xrge0adddir 33024 isros 34170 bnj964 34958 bnj1033 34984 cusgr3cyclex 35142 dfon2lem7 35791 outsideofcom 36130 linecom 36152 linerflx2 36153 topdifinffinlem 37349 rdgeqoa 37372 ishlat2 39355 lhpex2leN 40016 aks6d1c1rh 42127 sn-isghm 42688 lmbr3v 45765 lmbr3 45767 fourierdlem103 46229 fourierdlem104 46230 issmf 46748 issmff 46754 issmfle 46765 issmfgt 46776 issmfge 46790 grtriproplem 47911 grtrif1o 47914 funcf2lem 48930 | 
| Copyright terms: Public domain | W3C validator |