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  1648  fvtp0  7202  f13dfv  7278  poxp2  8144  xpord3lem  8150  poxp3  8151  xpord3pred  8153  axgroth5  10836  axgroth6  10840  hash7g  14553  cotr2g  15051  cbvprod  16004  cbvprodv  16005  prodeq1i  16007  isstruct  17248  pmtr3ncomlem1  19601  opprsubg  20494  addcuts  28241  mulcut  28395  ons2ind  28538  issubgr  29717  nbgrsym  29809  nb3grpr  29828  cplgr3v  29881  usgr2pthlem  30214  umgr2adedgwlk  30399  usgrwwlks2on  30412  umgrwwlks2on  30413  elwspths2spth  30424  clwwlkccat  30446  clwlkclwwlk  30458  3wlkdlem8  30633  frgr3v  30741  or3dir  32923  unelldsys  34656  bnj156  35225  bnj206  35228  bnj887  35262  bnj121  35366  bnj130  35370  bnj605  35403  bnj581  35404  brpprod3b  36451  brapply  36502  brrestrict  36515  dfrdg4  36517  brsegle  36675  prodeq2si  36811  cbvprodvw2  36854  dfeqvrels3  39408  tendoset  41619  grtriproplem  48842  grtrif1o  48845  usgrexmpl2trifr  48940  gpg5nbgrvtx03starlem1  48971  gpg5nbgrvtx03starlem2  48972  gpg5nbgrvtx03starlem3  48973  gpg5nbgrvtx13starlem1  48974  gpg5nbgrvtx13starlem2  48975  gpg5nbgrvtx13starlem3  48976  gpg5edgnedg  49033  2arwcatlem1  50508  setc1onsubc  50515