Theorem 3anbi123i 1156

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3anbi1i  1158  3anbi2i  1159  3anbi3i  1160  syl3anb  1162  an33rean  1486  cadnot  1617  f13dfv  7229  poxp2  8093  xpord3lem  8099  poxp3  8100  xpord3pred  8102  axgroth5  10747  axgroth6  10751  hash7g  14448  cotr2g  14938  cbvprod  15878  cbvprodv  15879  prodeq1i  15881  isstruct  17122  pmtr3ncomlem1  19448  opprsubg  20332  addcuts  27970  mulcut  28124  ons2ind  28267  issubgr  29340  nbgrsym  29432  nb3grpr  29451  cplgr3v  29504  usgr2pthlem  29831  umgr2adedgwlk  30013  usgrwwlks2on  30026  umgrwwlks2on  30027  elwspths2spth  30038  clwwlkccat  30060  clwlkclwwlk  30072  3wlkdlem8  30237  frgr3v  30345  or3dir  32529  unelldsys  34302  bnj156  34871  bnj206  34874  bnj887  34908  bnj121  35012  bnj130  35016  bnj605  35049  bnj581  35050  brpprod3b  36067  brapply  36118  brrestrict  36131  dfrdg4  36133  brsegle  36290  prodeq2si  36386  cbvprodvw2  36429  dfeqvrels3  38994  tendoset  41205  grtriproplem  48415  grtrif1o  48418  usgrexmpl2trifr  48513  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpg5edgnedg  48606  2arwcatlem1  50070  setc1onsubc  50077