Theorem 3anbi123i 1154

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  1156  3anbi2i  1157  3anbi3i  1158  syl3anb  1160  an33rean  1482  cadnot  1611  f13dfv  7293  poxp2  8166  xpord3lem  8172  poxp3  8173  xpord3pred  8175  axgroth5  10861  axgroth6  10865  hash7g  14521  cotr2g  15011  cbvprod  15945  cbvprodv  15946  prodeq1i  15948  isstruct  17185  pmtr3ncomlem1  19505  opprsubg  20368  addscut  28025  mulscut  28172  issubgr  29302  nbgrsym  29394  nb3grpr  29413  cplgr3v  29466  usgr2pthlem  29795  umgr2adedgwlk  29974  umgrwwlks2on  29986  elwspths2spth  29996  clwwlkccat  30018  clwlkclwwlk  30030  3wlkdlem8  30195  frgr3v  30303  or3dir  32488  unelldsys  34138  bnj156  34720  bnj206  34723  bnj887  34757  bnj121  34862  bnj130  34866  bnj605  34899  bnj581  34900  brpprod3b  35868  brapply  35919  brrestrict  35930  dfrdg4  35932  brsegle  36089  prodeq2si  36185  cbvprodvw2  36229  dfeqvrels3  38570  tendoset  40741  grtriproplem  47843  grtrif1o  47846  grlimgrtrilem1  47896  usgrexmpl2trifr  47931  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963