Theorem 3anbi123i 1171

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 639	. . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
4		bi3.3	. . 3 ⊢ (𝜏 ↔ 𝜂)
5	3, 4	anbi12i 639	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜏) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
6		df-3an 1103	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜏))
7		df-3an 1103	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
8	5, 6, 7	3bitr4i 306	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  3anbi1i  1173  3anbi2i  1174  3anbi3i  1175  syl3anb  1177  an33rean  1511  cadnot  1642  f13dfv  7273  poxp2  8139  xpord3lem  8145  poxp3  8146  xpord3pred  8148  axgroth5  10809  axgroth6  10813  hash7g  14523  cotr2g  15013  cbvprod  15967  cbvprodv  15968  prodeq1i  15970  isstruct  17212  pmtr3ncomlem1  19543  opprsubg  20434  addcuts  28137  mulcut  28291  ons2ind  28434  issubgr  29562  nbgrsym  29654  nb3grpr  29673  cplgr3v  29726  usgr2pthlem  30053  umgr2adedgwlk  30235  usgrwwlks2on  30248  umgrwwlks2on  30249  elwspths2spth  30260  clwwlkccat  30282  clwlkclwwlk  30294  3wlkdlem8  30459  frgr3v  30567  or3dir  32749  unelldsys  34493  bnj156  35062  bnj206  35065  bnj887  35099  bnj121  35203  bnj130  35207  bnj605  35240  bnj581  35241  brpprod3b  36310  brapply  36361  brrestrict  36374  dfrdg4  36376  brsegle  36533  prodeq2si  36639  cbvprodvw2  36682  dfeqvrels3  39247  tendoset  41458  grtriproplem  48628  grtrif1o  48631  usgrexmpl2trifr  48726  gpg5nbgrvtx03starlem1  48757  gpg5nbgrvtx03starlem2  48758  gpg5nbgrvtx03starlem3  48759  gpg5nbgrvtx13starlem1  48760  gpg5nbgrvtx13starlem2  48761  gpg5nbgrvtx13starlem3  48762  gpg5edgnedg  48819  2arwcatlem1  50293  setc1onsubc  50300