Theorem 3anbi123i 1173

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anbi1i  1175  3anbi2i  1176  3anbi3i  1177  syl3anb  1179  an33rean  1514  cadnot  1647  fvtp0  7206  f13dfv  7282  poxp2  8160  xpord3lem  8166  poxp3  8167  xpord3pred  8169  axgroth5  10909  axgroth6  10913  hash7g  14631  cotr2g  15129  cbvprod  16082  cbvprodv  16083  prodeq1i  16085  isstruct  17330  pmtr3ncomlem1  19687  opprsubg  20582  addcuts  28364  mulcut  28518  ons2ind  28661  issubgr  29852  nbgrsym  29944  nb3grpr  29963  cplgr3v  30016  usgr2pthlem  30349  umgr2adedgwlk  30534  usgrwwlks2on  30547  umgrwwlks2on  30548  elwspths2spth  30559  clwwlkccat  30581  clwlkclwwlk  30593  3wlkdlem8  30768  frgr3v  30876  or3dir  33058  unelldsys  34791  bnj156  35359  bnj206  35362  bnj887  35396  bnj121  35500  bnj130  35504  bnj605  35537  bnj581  35538  brpprod3b  36649  brapply  36700  brrestrict  36713  dfrdg4  36715  brsegle  36873  prodeq2si  36993  cbvprodvw2  37036  dfeqvrels3  39606  tendoset  41817  grtriproplem  49037  grtrif1o  49040  usgrexmpl2trifr  49135  gpg5nbgrvtx03starlem1  49166  gpg5nbgrvtx03starlem2  49167  gpg5nbgrvtx03starlem3  49168  gpg5nbgrvtx13starlem1  49169  gpg5nbgrvtx13starlem2  49170  gpg5nbgrvtx13starlem3  49171  gpg5edgnedg  49228  2arwcatlem1  50703  setc1onsubc  50710