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  1615  f13dfv  7211  poxp2  8076  xpord3lem  8082  poxp3  8083  xpord3pred  8085  axgroth5  10718  axgroth6  10722  hash7g  14393  cotr2g  14883  cbvprod  15820  cbvprodv  15821  prodeq1i  15823  isstruct  17063  pmtr3ncomlem1  19352  opprsubg  20237  addscut  27890  mulscut  28040  issubgr  29216  nbgrsym  29308  nb3grpr  29327  cplgr3v  29380  usgr2pthlem  29708  umgr2adedgwlk  29890  umgrwwlks2on  29902  elwspths2spth  29912  clwwlkccat  29934  clwlkclwwlk  29946  3wlkdlem8  30111  frgr3v  30219  or3dir  32404  unelldsys  34131  bnj156  34701  bnj206  34704  bnj887  34738  bnj121  34843  bnj130  34847  bnj605  34880  bnj581  34881  brpprod3b  35871  brapply  35922  brrestrict  35933  dfrdg4  35935  brsegle  36092  prodeq2si  36188  cbvprodvw2  36231  dfeqvrels3  38576  tendoset  40748  grtriproplem  47933  grtrif1o  47936  usgrexmpl2trifr  48031  gpg5nbgrvtx03starlem1  48062  gpg5nbgrvtx03starlem2  48063  gpg5nbgrvtx03starlem3  48064  gpg5nbgrvtx13starlem1  48065  gpg5nbgrvtx13starlem2  48066  gpg5nbgrvtx13starlem3  48067  gpg5edgnedg  48124  2arwcatlem1  49590  setc1onsubc  49597