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 630 | . . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)) |
4 | bi3.3 | . . 3 ⊢ (𝜏 ↔ 𝜂) | |
5 | 3, 4 | anbi12i 630 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜏) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂)) |
6 | df-3an 1091 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜏)) | |
7 | df-3an 1091 | . 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂)) | |
8 | 5, 6, 7 | 3bitr4i 306 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: 3anbi1i 1159 3anbi2i 1160 3anbi3i 1161 syl3anb 1163 an33rean 1485 an33reanOLD 1486 cadnot 1622 f13dfv 7082 axgroth5 10435 axgroth6 10439 cotr2g 14536 cbvprod 15474 isstruct 16702 pmtr3ncomlem1 18862 opprsubg 19651 issubgr 27356 nbgrsym 27448 nb3grpr 27467 cplgr3v 27520 usgr2pthlem 27847 umgr2adedgwlk 28026 umgrwwlks2on 28038 elwspths2spth 28048 clwwlkccat 28070 clwlkclwwlk 28082 3wlkdlem8 28247 frgr3v 28355 or3dir 30527 unelldsys 31835 bnj156 32416 bnj206 32419 bnj887 32454 bnj121 32560 bnj130 32564 bnj605 32597 bnj581 32598 poxp2 33524 xpord3lem 33529 poxp3 33530 brpprod3b 33923 brapply 33974 brrestrict 33985 dfrdg4 33987 brsegle 34144 dfeqvrels3 36437 tendoset 38508 |
Copyright terms: Public domain | W3C validator |