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  7249  poxp2  8122  xpord3lem  8128  poxp3  8129  xpord3pred  8131  axgroth5  10777  axgroth6  10781  hash7g  14451  cotr2g  14942  cbvprod  15879  cbvprodv  15880  prodeq1i  15882  isstruct  17122  pmtr3ncomlem1  19403  opprsubg  20261  addscut  27885  mulscut  28035  issubgr  29198  nbgrsym  29290  nb3grpr  29309  cplgr3v  29362  usgr2pthlem  29693  umgr2adedgwlk  29875  umgrwwlks2on  29887  elwspths2spth  29897  clwwlkccat  29919  clwlkclwwlk  29931  3wlkdlem8  30096  frgr3v  30204  or3dir  32389  unelldsys  34148  bnj156  34718  bnj206  34721  bnj887  34755  bnj121  34860  bnj130  34864  bnj605  34897  bnj581  34898  brpprod3b  35875  brapply  35926  brrestrict  35937  dfrdg4  35939  brsegle  36096  prodeq2si  36192  cbvprodvw2  36235  dfeqvrels3  38580  tendoset  40753  grtriproplem  47938  grtrif1o  47941  grlimgrtrilem1  47993  usgrexmpl2trifr  48028  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  2arwcatlem1  49584  setc1onsubc  49591