Theorem 3anbi123i 1148

Description: Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.)

Hypotheses

Ref	Expression
bi3.1	⊢ (𝜑 ↔ 𝜓)
bi3.2	⊢ (𝜒 ↔ 𝜃)
bi3.3	⊢ (𝜏 ↔ 𝜂)

Assertion

Ref	Expression
3anbi123i	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂))

Proof of Theorem 3anbi123i

Step	Hyp	Ref	Expression
1		bi3.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2		bi3.2	. . . 4 ⊢ (𝜒 ↔ 𝜃)
3	1, 2	anbi12i 626	. . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
4		bi3.3	. . 3 ⊢ (𝜏 ↔ 𝜂)
5	3, 4	anbi12i 626	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜏) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
6		df-3an 1082	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜏))
7		df-3an 1082	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
8	5, 6, 7	3bitr4i 304	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂))

Syntax hints:   ↔ wb 207   ∧ wa 396   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  3anbi1i  1150  3anbi2i  1151  3anbi3i  1152  syl3anb  1154  an33rean  1475  cadnot  1597  f13dfv  6896  axgroth5  10092  axgroth6  10096  cotr2g  14170  cbvprod  15102  isstruct  16325  pmtr3ncomlem1  18332  opprsubg  19076  issubgr  26736  nbgrsym  26828  nb3grpr  26847  cplgr3v  26900  usgr2pthlem  27231  umgr2adedgwlk  27411  umgrwwlks2on  27423  elwspths2spth  27433  clwwlkccat  27455  clwlkclwwlk  27467  3wlkdlem8  27633  frgr3v  27746  or3dir  29917  unelldsys  31034  bnj156  31615  bnj206  31618  bnj887  31653  bnj121  31758  bnj130  31762  bnj605  31795  bnj581  31796  brpprod3b  32957  brapply  33008  brrestrict  33019  dfrdg4  33021  brsegle  33178  dfeqvrels3  35355  tendoset  37426