Theorem 3anbi123i 1155

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

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

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 1088

This theorem is referenced by:  3anbi1i  1157  3anbi2i  1158  3anbi3i  1159  syl3anb  1161  an33rean  1485  cadnot  1616  f13dfv  7208  poxp2  8073  xpord3lem  8079  poxp3  8080  xpord3pred  8082  axgroth5  10715  axgroth6  10719  hash7g  14393  cotr2g  14883  cbvprod  15820  cbvprodv  15821  prodeq1i  15823  isstruct  17063  pmtr3ncomlem1  19385  opprsubg  20270  addscut  27921  mulscut  28071  issubgr  29249  nbgrsym  29341  nb3grpr  29360  cplgr3v  29413  usgr2pthlem  29741  umgr2adedgwlk  29923  usgrwwlks2on  29936  umgrwwlks2on  29937  elwspths2spth  29948  clwwlkccat  29970  clwlkclwwlk  29982  3wlkdlem8  30147  frgr3v  30255  or3dir  32439  unelldsys  34171  bnj156  34740  bnj206  34743  bnj887  34777  bnj121  34882  bnj130  34886  bnj605  34919  bnj581  34920  brpprod3b  35929  brapply  35980  brrestrict  35993  dfrdg4  35995  brsegle  36152  prodeq2si  36248  cbvprodvw2  36291  dfeqvrels3  38684  tendoset  40857  grtriproplem  48038  grtrif1o  48041  usgrexmpl2trifr  48136  gpg5nbgrvtx03starlem1  48167  gpg5nbgrvtx03starlem2  48168  gpg5nbgrvtx03starlem3  48169  gpg5nbgrvtx13starlem1  48170  gpg5nbgrvtx13starlem2  48171  gpg5nbgrvtx13starlem3  48172  gpg5edgnedg  48229  2arwcatlem1  49695  setc1onsubc  49702