Theorem 3anbi123i 1172

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 400   ∧ w3a 1102

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 401  df-3an 1104

This theorem is used by:  3anbi1i  1174  3anbi2i  1175  3anbi3i  1176  syl3anb  1178  an33rean  1513  cadnot  1644  f13dfv  7272  poxp2  8137  xpord3lem  8143  poxp3  8144  xpord3pred  8146  axgroth5  10815  axgroth6  10819  hash7g  14530  cotr2g  15020  cbvprod  15974  cbvprodv  15975  prodeq1i  15977  isstruct  17218  pmtr3ncomlem1  19549  opprsubg  20441  addcuts  28182  mulcut  28336  ons2ind  28479  issubgr  29632  nbgrsym  29724  nb3grpr  29743  cplgr3v  29796  usgr2pthlem  30123  umgr2adedgwlk  30305  usgrwwlks2on  30318  umgrwwlks2on  30319  elwspths2spth  30330  clwwlkccat  30352  clwlkclwwlk  30364  3wlkdlem8  30529  frgr3v  30637  or3dir  32819  unelldsys  34557  bnj156  35126  bnj206  35129  bnj887  35163  bnj121  35267  bnj130  35271  bnj605  35304  bnj581  35305  brpprod3b  36385  brapply  36436  brrestrict  36449  dfrdg4  36451  brsegle  36608  prodeq2si  36744  cbvprodvw2  36787  dfeqvrels3  39350  tendoset  41561  grtriproplem  48732  grtrif1o  48735  usgrexmpl2trifr  48830  gpg5nbgrvtx03starlem1  48861  gpg5nbgrvtx03starlem2  48862  gpg5nbgrvtx03starlem3  48863  gpg5nbgrvtx13starlem1  48864  gpg5nbgrvtx13starlem2  48865  gpg5nbgrvtx13starlem3  48866  gpg5edgnedg  48923  2arwcatlem1  50401  setc1onsubc  50408