|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > 3anbi123i | Structured version Visualization version GIF version | ||
| Description: Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.) | 
| Ref | Expression | 
|---|---|
| bi3.1 | ⊢ (𝜑 ↔ 𝜓) | 
| bi3.2 | ⊢ (𝜒 ↔ 𝜃) | 
| bi3.3 | ⊢ (𝜏 ↔ 𝜂) | 
| Ref | Expression | 
|---|---|
| 3anbi123i | ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | bi3.1 | . . . 4 ⊢ (𝜑 ↔ 𝜓) | |
| 2 | bi3.2 | . . . 4 ⊢ (𝜒 ↔ 𝜃) | |
| 3 | 1, 2 | anbi12i 628 | . . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)) | 
| 4 | bi3.3 | . . 3 ⊢ (𝜏 ↔ 𝜂) | |
| 5 | 3, 4 | anbi12i 628 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜏) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂)) | 
| 6 | df-3an 1089 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜏)) | |
| 7 | df-3an 1089 | . 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂)) | |
| 8 | 5, 6, 7 | 3bitr4i 303 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∧ wa 395 ∧ 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 207 df-an 396 df-3an 1089 | 
| This theorem is referenced by: 3anbi1i 1158 3anbi2i 1159 3anbi3i 1160 syl3anb 1162 an33rean 1485 cadnot 1615 f13dfv 7294 poxp2 8168 xpord3lem 8174 poxp3 8175 xpord3pred 8177 axgroth5 10864 axgroth6 10868 hash7g 14525 cotr2g 15015 cbvprod 15949 cbvprodv 15950 prodeq1i 15952 isstruct 17189 pmtr3ncomlem1 19491 opprsubg 20352 addscut 28011 mulscut 28158 issubgr 29288 nbgrsym 29380 nb3grpr 29399 cplgr3v 29452 usgr2pthlem 29783 umgr2adedgwlk 29965 umgrwwlks2on 29977 elwspths2spth 29987 clwwlkccat 30009 clwlkclwwlk 30021 3wlkdlem8 30186 frgr3v 30294 or3dir 32479 unelldsys 34159 bnj156 34742 bnj206 34745 bnj887 34779 bnj121 34884 bnj130 34888 bnj605 34921 bnj581 34922 brpprod3b 35888 brapply 35939 brrestrict 35950 dfrdg4 35952 brsegle 36109 prodeq2si 36205 cbvprodvw2 36248 dfeqvrels3 38590 tendoset 40761 grtriproplem 47906 grtrif1o 47909 grlimgrtrilem1 47961 usgrexmpl2trifr 47996 gpg5nbgrvtx03starlem1 48024 gpg5nbgrvtx03starlem2 48025 gpg5nbgrvtx03starlem3 48026 gpg5nbgrvtx13starlem1 48027 gpg5nbgrvtx13starlem2 48028 gpg5nbgrvtx13starlem3 48029 | 
| Copyright terms: Public domain | W3C validator |