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

Syntax hints:   ↔ wb 205   ∧ wa 397   ∧ w3a 1088

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

This theorem is referenced by:  3anbi1i  1158  3anbi2i  1159  3anbi3i  1160  syl3anb  1162  an33rean  1484  an33reanOLD  1485  cadnot  1617  f13dfv  7215  axgroth5  10694  axgroth6  10698  cotr2g  14796  cbvprod  15734  isstruct  16960  pmtr3ncomlem1  19190  opprsubg  19994  issubgr  28024  nbgrsym  28116  nb3grpr  28135  cplgr3v  28188  usgr2pthlem  28516  umgr2adedgwlk  28695  umgrwwlks2on  28707  elwspths2spth  28717  clwwlkccat  28739  clwlkclwwlk  28751  3wlkdlem8  28916  frgr3v  29024  or3dir  31196  unelldsys  32537  bnj156  33120  bnj206  33123  bnj887  33157  bnj121  33262  bnj130  33266  bnj605  33299  bnj581  33300  poxp2  34182  xpord3lem  34187  poxp3  34188  xpord3pred  34190  brpprod3b  34403  brapply  34454  brrestrict  34465  dfrdg4  34467  brsegle  34624  dfeqvrels3  36982  tendoset  39153