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  7252  poxp2  8125  xpord3lem  8131  poxp3  8132  xpord3pred  8134  axgroth5  10784  axgroth6  10788  hash7g  14458  cotr2g  14949  cbvprod  15886  cbvprodv  15887  prodeq1i  15889  isstruct  17129  pmtr3ncomlem1  19410  opprsubg  20268  addscut  27892  mulscut  28042  issubgr  29205  nbgrsym  29297  nb3grpr  29316  cplgr3v  29369  usgr2pthlem  29700  umgr2adedgwlk  29882  umgrwwlks2on  29894  elwspths2spth  29904  clwwlkccat  29926  clwlkclwwlk  29938  3wlkdlem8  30103  frgr3v  30211  or3dir  32396  unelldsys  34155  bnj156  34725  bnj206  34728  bnj887  34762  bnj121  34867  bnj130  34871  bnj605  34904  bnj581  34905  brpprod3b  35882  brapply  35933  brrestrict  35944  dfrdg4  35946  brsegle  36103  prodeq2si  36199  cbvprodvw2  36242  dfeqvrels3  38587  tendoset  40760  grtriproplem  47942  grtrif1o  47945  grlimgrtrilem1  47997  usgrexmpl2trifr  48032  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  2arwcatlem1  49588  setc1onsubc  49595