Theorem 3anbi123i 1153

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

Syntax hints:   ↔ wb 205   ∧ wa 394   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  3anbi1i  1155  3anbi2i  1156  3anbi3i  1157  syl3anb  1159  an33rean  1481  an33reanOLD  1482  cadnot  1614  f13dfv  7274  poxp2  8131  xpord3lem  8137  poxp3  8138  xpord3pred  8140  axgroth5  10821  axgroth6  10825  cotr2g  14927  cbvprod  15863  isstruct  17089  pmtr3ncomlem1  19382  opprsubg  20243  addscut  27700  mulscut  27827  issubgr  28795  nbgrsym  28887  nb3grpr  28906  cplgr3v  28959  usgr2pthlem  29287  umgr2adedgwlk  29466  umgrwwlks2on  29478  elwspths2spth  29488  clwwlkccat  29510  clwlkclwwlk  29522  3wlkdlem8  29687  frgr3v  29795  or3dir  31969  unelldsys  33454  bnj156  34037  bnj206  34040  bnj887  34074  bnj121  34179  bnj130  34183  bnj605  34216  bnj581  34217  brpprod3b  35163  brapply  35214  brrestrict  35225  dfrdg4  35227  brsegle  35384  dfeqvrels3  37762  tendoset  39933