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  7195  f13dfv  7271  poxp2  8139  xpord3lem  8145  poxp3  8146  xpord3pred  8148  axgroth5  10866  axgroth6  10870  hash7g  14584  cotr2g  15082  cbvprod  16035  cbvprodv  16036  prodeq1i  16038  isstruct  17277  pmtr3ncomlem1  19634  opprsubg  20529  addcuts  28283  mulcut  28437  ons2ind  28580  issubgr  29771  nbgrsym  29863  nb3grpr  29882  cplgr3v  29935  usgr2pthlem  30268  umgr2adedgwlk  30453  usgrwwlks2on  30466  umgrwwlks2on  30467  elwspths2spth  30478  clwwlkccat  30500  clwlkclwwlk  30512  3wlkdlem8  30687  frgr3v  30795  or3dir  32977  unelldsys  34710  bnj156  35279  bnj206  35282  bnj887  35316  bnj121  35420  bnj130  35424  bnj605  35457  bnj581  35458  brpprod3b  36565  brapply  36616  brrestrict  36629  dfrdg4  36631  brsegle  36789  prodeq2si  36909  cbvprodvw2  36952  dfeqvrels3  39519  tendoset  41730  grtriproplem  48953  grtrif1o  48956  usgrexmpl2trifr  49051  gpg5nbgrvtx03starlem1  49082  gpg5nbgrvtx03starlem2  49083  gpg5nbgrvtx03starlem3  49084  gpg5nbgrvtx13starlem1  49085  gpg5nbgrvtx13starlem2  49086  gpg5nbgrvtx13starlem3  49087  gpg5edgnedg  49144  2arwcatlem1  50619  setc1onsubc  50626