Theorem 3anbi123i 1162

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

Syntax hints:   ↔ wb 208   ∧ wa 397   ∧ w3a 1093

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 209  df-an 398  df-3an 1095

This theorem is referenced by:  3anbi1i  1164  3anbi2i  1165  3anbi3i  1166  syl3anb  1168  an33rean  1492  cadnot  1623  f13dfv  7222  poxp2  8087  xpord3lem  8093  poxp3  8094  xpord3pred  8096  axgroth5  10742  axgroth6  10746  hash7g  14443  cotr2g  14933  cbvprod  15873  cbvprodv  15874  prodeq1i  15876  isstruct  17117  pmtr3ncomlem1  19443  opprsubg  20327  addcuts  27992  mulcut  28146  ons2ind  28289  issubgr  29362  nbgrsym  29454  nb3grpr  29473  cplgr3v  29526  usgr2pthlem  29853  umgr2adedgwlk  30035  usgrwwlks2on  30048  umgrwwlks2on  30049  elwspths2spth  30060  clwwlkccat  30082  clwlkclwwlk  30094  3wlkdlem8  30259  frgr3v  30367  or3dir  32551  unelldsys  34354  bnj156  34926  bnj206  34929  bnj887  34963  bnj121  35067  bnj130  35071  bnj605  35104  bnj581  35105  brpprod3b  36128  brapply  36179  brrestrict  36192  dfrdg4  36194  brsegle  36351  prodeq2si  36447  cbvprodvw2  36490  dfeqvrels3  39055  tendoset  41266  grtriproplem  48444  grtrif1o  48447  usgrexmpl2trifr  48542  gpg5nbgrvtx03starlem1  48573  gpg5nbgrvtx03starlem2  48574  gpg5nbgrvtx03starlem3  48575  gpg5nbgrvtx13starlem1  48576  gpg5nbgrvtx13starlem2  48577  gpg5nbgrvtx13starlem3  48578  gpg5edgnedg  48635  2arwcatlem1  50099  setc1onsubc  50106