Theorem 3anbi123i 1169

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

Syntax hints:   ↔ wb 208   ∧ wa 399   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  3anbi1i  1171  3anbi2i  1172  3anbi3i  1173  syl3anb  1175  an33rean  1506  cadnot  1637  f13dfv  7260  poxp2  8125  xpord3lem  8131  poxp3  8132  xpord3pred  8134  axgroth5  10784  axgroth6  10788  hash7g  14501  cotr2g  14991  cbvprod  15945  cbvprodv  15946  prodeq1i  15948  isstruct  17190  pmtr3ncomlem1  19515  opprsubg  20403  addcuts  28073  mulcut  28227  ons2ind  28370  issubgr  29474  nbgrsym  29566  nb3grpr  29585  cplgr3v  29638  usgr2pthlem  29965  umgr2adedgwlk  30147  usgrwwlks2on  30160  umgrwwlks2on  30161  elwspths2spth  30172  clwwlkccat  30194  clwlkclwwlk  30206  3wlkdlem8  30371  frgr3v  30479  or3dir  32662  unelldsys  34457  bnj156  35026  bnj206  35029  bnj887  35063  bnj121  35167  bnj130  35171  bnj605  35204  bnj581  35205  brpprod3b  36240  brapply  36291  brrestrict  36304  dfrdg4  36306  brsegle  36463  prodeq2si  36569  cbvprodvw2  36612  dfeqvrels3  39177  tendoset  41388  grtriproplem  48566  grtrif1o  48569  usgrexmpl2trifr  48664  gpg5nbgrvtx03starlem1  48695  gpg5nbgrvtx03starlem2  48696  gpg5nbgrvtx03starlem3  48697  gpg5nbgrvtx13starlem1  48698  gpg5nbgrvtx13starlem2  48699  gpg5nbgrvtx13starlem3  48700  gpg5edgnedg  48757  2arwcatlem1  50221  setc1onsubc  50228