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  7222  poxp2  8087  xpord3lem  8093  poxp3  8094  xpord3pred  8096  axgroth5  10739  axgroth6  10743  hash7g  14413  cotr2g  14903  cbvprod  15840  cbvprodv  15841  prodeq1i  15843  isstruct  17083  pmtr3ncomlem1  19406  opprsubg  20292  addcuts  27978  mulcut  28132  ons2ind  28275  issubgr  29348  nbgrsym  29440  nb3grpr  29459  cplgr3v  29512  usgr2pthlem  29840  umgr2adedgwlk  30022  usgrwwlks2on  30035  umgrwwlks2on  30036  elwspths2spth  30047  clwwlkccat  30069  clwlkclwwlk  30081  3wlkdlem8  30246  frgr3v  30354  or3dir  32537  unelldsys  34317  bnj156  34886  bnj206  34889  bnj887  34923  bnj121  35028  bnj130  35032  bnj605  35065  bnj581  35066  brpprod3b  36081  brapply  36132  brrestrict  36145  dfrdg4  36147  brsegle  36304  prodeq2si  36400  cbvprodvw2  36443  dfeqvrels3  38876  tendoset  41087  grtriproplem  48252  grtrif1o  48255  usgrexmpl2trifr  48350  gpg5nbgrvtx03starlem1  48381  gpg5nbgrvtx03starlem2  48382  gpg5nbgrvtx03starlem3  48383  gpg5nbgrvtx13starlem1  48384  gpg5nbgrvtx13starlem2  48385  gpg5nbgrvtx13starlem3  48386  gpg5edgnedg  48443  2arwcatlem1  49907  setc1onsubc  49914