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  7231  poxp2  8099  xpord3lem  8105  poxp3  8106  xpord3pred  8108  axgroth5  10753  axgroth6  10757  hash7g  14427  cotr2g  14918  cbvprod  15855  cbvprodv  15856  prodeq1i  15858  isstruct  17098  pmtr3ncomlem1  19387  opprsubg  20272  addscut  27925  mulscut  28075  issubgr  29251  nbgrsym  29343  nb3grpr  29362  cplgr3v  29415  usgr2pthlem  29743  umgr2adedgwlk  29925  umgrwwlks2on  29937  elwspths2spth  29947  clwwlkccat  29969  clwlkclwwlk  29981  3wlkdlem8  30146  frgr3v  30254  or3dir  32439  unelldsys  34141  bnj156  34711  bnj206  34714  bnj887  34748  bnj121  34853  bnj130  34857  bnj605  34890  bnj581  34891  brpprod3b  35868  brapply  35919  brrestrict  35930  dfrdg4  35932  brsegle  36089  prodeq2si  36185  cbvprodvw2  36228  dfeqvrels3  38573  tendoset  40746  grtriproplem  47931  grtrif1o  47934  grlimgrtrilem1  47986  usgrexmpl2trifr  48021  gpg5nbgrvtx03starlem1  48052  gpg5nbgrvtx03starlem2  48053  gpg5nbgrvtx03starlem3  48054  gpg5nbgrvtx13starlem1  48055  gpg5nbgrvtx13starlem2  48056  gpg5nbgrvtx13starlem3  48057  2arwcatlem1  49577  setc1onsubc  49584