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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∧ w3a 1087

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 1089

This theorem is referenced by:  3anbi1i  1157  3anbi2i  1158  3anbi3i  1159  syl3anb  1161  an33rean  1483  an33reanOLD  1484  cadnot  1616  f13dfv  7271  poxp2  8128  xpord3lem  8134  poxp3  8135  xpord3pred  8137  axgroth5  10818  axgroth6  10822  cotr2g  14922  cbvprod  15858  isstruct  17084  pmtr3ncomlem1  19340  opprsubg  20165  addscut  27459  mulscut  27585  issubgr  28525  nbgrsym  28617  nb3grpr  28636  cplgr3v  28689  usgr2pthlem  29017  umgr2adedgwlk  29196  umgrwwlks2on  29208  elwspths2spth  29218  clwwlkccat  29240  clwlkclwwlk  29252  3wlkdlem8  29417  frgr3v  29525  or3dir  31697  unelldsys  33151  bnj156  33734  bnj206  33737  bnj887  33771  bnj121  33876  bnj130  33880  bnj605  33913  bnj581  33914  brpprod3b  34854  brapply  34905  brrestrict  34916  dfrdg4  34918  brsegle  35075  dfeqvrels3  37454  tendoset  39625