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  7232  poxp2  8097  xpord3lem  8103  poxp3  8104  xpord3pred  8106  axgroth5  10749  axgroth6  10753  hash7g  14423  cotr2g  14913  cbvprod  15850  cbvprodv  15851  prodeq1i  15853  isstruct  17093  pmtr3ncomlem1  19419  opprsubg  20305  addcuts  27991  mulcut  28145  ons2ind  28288  issubgr  29362  nbgrsym  29454  nb3grpr  29473  cplgr3v  29526  usgr2pthlem  29854  umgr2adedgwlk  30036  usgrwwlks2on  30049  umgrwwlks2on  30050  elwspths2spth  30061  clwwlkccat  30083  clwlkclwwlk  30095  3wlkdlem8  30260  frgr3v  30368  or3dir  32552  unelldsys  34342  bnj156  34911  bnj206  34914  bnj887  34948  bnj121  35052  bnj130  35056  bnj605  35089  bnj581  35090  brpprod3b  36107  brapply  36158  brrestrict  36171  dfrdg4  36173  brsegle  36330  prodeq2si  36426  cbvprodvw2  36469  dfeqvrels3  38953  tendoset  41164  grtriproplem  48328  grtrif1o  48331  usgrexmpl2trifr  48426  gpg5nbgrvtx03starlem1  48457  gpg5nbgrvtx03starlem2  48458  gpg5nbgrvtx03starlem3  48459  gpg5nbgrvtx13starlem1  48460  gpg5nbgrvtx13starlem2  48461  gpg5nbgrvtx13starlem3  48462  gpg5edgnedg  48519  2arwcatlem1  49983  setc1onsubc  49990