Theorem 3anbi123i 1173

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 640	. . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
4		bi3.3	. . 3 ⊢ (𝜏 ↔ 𝜂)
5	3, 4	anbi12i 640	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜏) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
6		df-3an 1105	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜏))
7		df-3an 1105	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
8	5, 6, 7	3bitr4i 306	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anbi1i  1175  3anbi2i  1176  3anbi3i  1177  syl3anb  1179  an33rean  1514  cadnot  1648  fvtp0  7203  f13dfv  7279  poxp2  8145  xpord3lem  8151  poxp3  8152  xpord3pred  8154  axgroth5  10837  axgroth6  10841  hash7g  14555  cotr2g  15053  cbvprod  16006  cbvprodv  16007  prodeq1i  16009  isstruct  17250  pmtr3ncomlem1  19606  opprsubg  20499  addcuts  28251  mulcut  28405  ons2ind  28548  issubgr  29739  nbgrsym  29831  nb3grpr  29850  cplgr3v  29903  usgr2pthlem  30236  umgr2adedgwlk  30421  usgrwwlks2on  30434  umgrwwlks2on  30435  elwspths2spth  30446  clwwlkccat  30468  clwlkclwwlk  30480  3wlkdlem8  30655  frgr3v  30763  or3dir  32945  unelldsys  34677  bnj156  35246  bnj206  35249  bnj887  35283  bnj121  35387  bnj130  35391  bnj605  35424  bnj581  35425  brpprod3b  36472  brapply  36523  brrestrict  36536  dfrdg4  36538  brsegle  36696  prodeq2si  36832  cbvprodvw2  36875  dfeqvrels3  39429  tendoset  41640  grtriproplem  48863  grtrif1o  48866  usgrexmpl2trifr  48961  gpg5nbgrvtx03starlem1  48992  gpg5nbgrvtx03starlem2  48993  gpg5nbgrvtx03starlem3  48994  gpg5nbgrvtx13starlem1  48995  gpg5nbgrvtx13starlem2  48996  gpg5nbgrvtx13starlem3  48997  gpg5edgnedg  49054  2arwcatlem1  50529  setc1onsubc  50536