Theorem 3anbi123i 1151

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

Syntax hints:   ↔ wb 208   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  3anbi1i  1153  3anbi2i  1154  3anbi3i  1155  syl3anb  1157  an33rean  1479  an33reanOLD  1480  cadnot  1616  f13dfv  7031  axgroth5  10246  axgroth6  10250  cotr2g  14336  cbvprod  15269  isstruct  16496  pmtr3ncomlem1  18601  opprsubg  19386  issubgr  27053  nbgrsym  27145  nb3grpr  27164  cplgr3v  27217  usgr2pthlem  27544  umgr2adedgwlk  27724  umgrwwlks2on  27736  elwspths2spth  27746  clwwlkccat  27768  clwlkclwwlk  27780  3wlkdlem8  27946  frgr3v  28054  or3dir  30226  unelldsys  31417  bnj156  31998  bnj206  32001  bnj887  32036  bnj121  32142  bnj130  32146  bnj605  32179  bnj581  32180  brpprod3b  33348  brapply  33399  brrestrict  33410  dfrdg4  33412  brsegle  33569  dfeqvrels3  35839  tendoset  37910