![]() |
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 733 | . . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)) |
4 | bi3.3 | . . 3 ⊢ (𝜏 ↔ 𝜂) | |
5 | 3, 4 | anbi12i 733 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜏) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂)) |
6 | df-3an 1056 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜏)) | |
7 | df-3an 1056 | . 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂)) | |
8 | 5, 6, 7 | 3bitr4i 292 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 ∧ w3a 1054 |
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 197 df-an 385 df-3an 1056 |
This theorem is referenced by: 3anbi1i 1272 3anbi2i 1273 3anbi3i 1274 syl3anb 1409 an33rean 1486 cadnot 1594 f13dfv 6570 axgroth5 9684 axgroth6 9688 cotr2g 13761 cbvprod 14689 isstruct 15917 pmtr3ncomlem1 17939 opprsubg 18682 issubgr 26208 nbgrsym 26308 nbgrsymOLD 26309 nb3grpr 26328 cplgr3v 26387 usgr2pthlem 26715 umgr2adedgwlk 26910 umgrwwlks2on 26923 elwspths2spth 26934 clwlkclwwlk 26968 clwlksfclwwlk 27049 3wlkdlem8 27145 frgr3v 27255 clwwlkccat 27332 or3dir 29436 unelldsys 30349 bnj156 30922 bnj206 30925 bnj887 30961 bnj121 31066 bnj130 31070 bnj605 31103 bnj581 31104 brpprod3b 32119 brapply 32170 brrestrict 32181 dfrdg4 32183 brsegle 32340 tendoset 36364 |
Copyright terms: Public domain | W3C validator |