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  1615  f13dfv  7267  poxp2  8142  xpord3lem  8148  poxp3  8149  xpord3pred  8151  axgroth5  10838  axgroth6  10842  hash7g  14504  cotr2g  14995  cbvprod  15929  cbvprodv  15930  prodeq1i  15932  isstruct  17171  pmtr3ncomlem1  19454  opprsubg  20312  addscut  27937  mulscut  28087  issubgr  29250  nbgrsym  29342  nb3grpr  29361  cplgr3v  29414  usgr2pthlem  29745  umgr2adedgwlk  29927  umgrwwlks2on  29939  elwspths2spth  29949  clwwlkccat  29971  clwlkclwwlk  29983  3wlkdlem8  30148  frgr3v  30256  or3dir  32441  unelldsys  34189  bnj156  34759  bnj206  34762  bnj887  34796  bnj121  34901  bnj130  34905  bnj605  34938  bnj581  34939  brpprod3b  35905  brapply  35956  brrestrict  35967  dfrdg4  35969  brsegle  36126  prodeq2si  36222  cbvprodvw2  36265  dfeqvrels3  38607  tendoset  40778  grtriproplem  47951  grtrif1o  47954  grlimgrtrilem1  48006  usgrexmpl2trifr  48041  gpg5nbgrvtx03starlem1  48070  gpg5nbgrvtx03starlem2  48071  gpg5nbgrvtx03starlem3  48072  gpg5nbgrvtx13starlem1  48073  gpg5nbgrvtx13starlem2  48074  gpg5nbgrvtx13starlem3  48075  2arwcatlem1  49472  setc1onsubc  49479