Theorem 3anbi123i 1154

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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3anbi1i  1156  3anbi2i  1157  3anbi3i  1158  syl3anb  1160  an33rean  1482  an33reanOLD  1483  cadnot  1617  f13dfv  7155  axgroth5  10589  axgroth6  10593  cotr2g  14696  cbvprod  15634  isstruct  16862  pmtr3ncomlem1  19090  opprsubg  19887  issubgr  27647  nbgrsym  27739  nb3grpr  27758  cplgr3v  27811  usgr2pthlem  28140  umgr2adedgwlk  28319  umgrwwlks2on  28331  elwspths2spth  28341  clwwlkccat  28363  clwlkclwwlk  28375  3wlkdlem8  28540  frgr3v  28648  or3dir  30820  unelldsys  32135  bnj156  32716  bnj206  32719  bnj887  32754  bnj121  32859  bnj130  32863  bnj605  32896  bnj581  32897  poxp2  33799  xpord3lem  33804  poxp3  33805  brpprod3b  34198  brapply  34249  brrestrict  34260  dfrdg4  34262  brsegle  34419  dfeqvrels3  36709  tendoset  38780