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  1515  cadnot  1648  fvtp0  7226  f13dfv  7302  poxp2  8184  xpord3lem  8190  poxp3  8191  xpord3pred  8193  axgroth5  10933  axgroth6  10937  hash7g  14655  cotr2g  15155  cbvprod  16108  cbvprodv  16109  prodeq1i  16111  isstruct  17356  pmtr3ncomlem1  19714  opprsubg  20609  addcuts  28391  mulcut  28545  ons2ind  28688  issubgr  29879  nbgrsym  29971  nb3grpr  29990  cplgr3v  30043  usgr2pthlem  30376  umgr2adedgwlk  30561  usgrwwlks2on  30574  umgrwwlks2on  30575  elwspths2spth  30586  clwwlkccat  30608  clwlkclwwlk  30620  3wlkdlem8  30795  frgr3v  30903  or3dir  33127  unelldsys  34858  bnj156  35426  bnj206  35429  bnj887  35463  bnj121  35567  bnj130  35571  bnj605  35604  bnj581  35605  brpprod3b  36826  brapply  36877  brrestrict  36890  dfrdg4  36892  brsegle  37050  prodeq2si  37170  cbvprodvw2  37213  dfeqvrels3  39796  tendoset  42007  grtriproplem  49240  grtrif1o  49243  usgrexmpl2trifr  49338  gpg5nbgrvtx03starlem1  49369  gpg5nbgrvtx03starlem2  49370  gpg5nbgrvtx03starlem3  49371  gpg5nbgrvtx13starlem1  49372  gpg5nbgrvtx13starlem2  49373  gpg5nbgrvtx13starlem3  49374  gpg5edgnedg  49431  2arwcatlem1  50936  setc1onsubc  50943