Theorem 3anbi123i 1155

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3anbi1i  1157  3anbi2i  1158  3anbi3i  1159  syl3anb  1161  an33rean  1485  cadnot  1616  f13dfv  7218  poxp2  8083  xpord3lem  8089  poxp3  8090  xpord3pred  8092  axgroth5  10733  axgroth6  10737  hash7g  14407  cotr2g  14897  cbvprod  15834  cbvprodv  15835  prodeq1i  15837  isstruct  17077  pmtr3ncomlem1  19400  opprsubg  20286  addscut  27948  mulscut  28101  issubgr  29293  nbgrsym  29385  nb3grpr  29404  cplgr3v  29457  usgr2pthlem  29785  umgr2adedgwlk  29967  usgrwwlks2on  29980  umgrwwlks2on  29981  elwspths2spth  29992  clwwlkccat  30014  clwlkclwwlk  30026  3wlkdlem8  30191  frgr3v  30299  or3dir  32483  unelldsys  34264  bnj156  34833  bnj206  34836  bnj887  34870  bnj121  34975  bnj130  34979  bnj605  35012  bnj581  35013  brpprod3b  36028  brapply  36079  brrestrict  36092  dfrdg4  36094  brsegle  36251  prodeq2si  36347  cbvprodvw2  36390  dfeqvrels3  38785  tendoset  40958  grtriproplem  48127  grtrif1o  48130  usgrexmpl2trifr  48225  gpg5nbgrvtx03starlem1  48256  gpg5nbgrvtx03starlem2  48257  gpg5nbgrvtx03starlem3  48258  gpg5nbgrvtx13starlem1  48259  gpg5nbgrvtx13starlem2  48260  gpg5nbgrvtx13starlem3  48261  gpg5edgnedg  48318  2arwcatlem1  49782  setc1onsubc  49789