![]() |
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 1090 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜏)) | |
7 | df-3an 1090 | . 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂)) | |
8 | 5, 6, 7 | 3bitr4i 303 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 ∧ w3a 1088 |
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 206 df-an 398 df-3an 1090 |
This theorem is referenced by: 3anbi1i 1158 3anbi2i 1159 3anbi3i 1160 syl3anb 1162 an33rean 1484 an33reanOLD 1485 cadnot 1617 f13dfv 7224 poxp2 8079 xpord3lem 8085 poxp3 8086 xpord3pred 8088 axgroth5 10768 axgroth6 10772 cotr2g 14870 cbvprod 15806 isstruct 17032 pmtr3ncomlem1 19263 opprsubg 20073 issubgr 28268 nbgrsym 28360 nb3grpr 28379 cplgr3v 28432 usgr2pthlem 28760 umgr2adedgwlk 28939 umgrwwlks2on 28951 elwspths2spth 28961 clwwlkccat 28983 clwlkclwwlk 28995 3wlkdlem8 29160 frgr3v 29268 or3dir 31440 unelldsys 32821 bnj156 33404 bnj206 33407 bnj887 33441 bnj121 33546 bnj130 33550 bnj605 33583 bnj581 33584 brpprod3b 34525 brapply 34576 brrestrict 34587 dfrdg4 34589 brsegle 34746 dfeqvrels3 37101 tendoset 39272 |
Copyright terms: Public domain | W3C validator |