Theorem 3anbi123i 1243

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

Syntax hints:   ↔ wb 194   ∧ wa 382   ∧ w3a 1030

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 195  df-an 384  df-3an 1032

This theorem is referenced by:  3anbi1i  1245  3anbi2i  1246  3anbi3i  1247  syl3anb  1360  an33rean  1437  cadnot  1544  f13dfv  6408  axgroth5  9502  axgroth6  9506  cotr2g  13509  cbvprod  14430  isstruct  15651  pmtr3ncomlem1  17662  opprsubg  18405  nb3grapr  25748  cusgra3v  25759  wwlknfi  26032  frgra3v  26295  or3dir  28498  unelldsys  29354  bnj156  29856  bnj206  29859  bnj887  29895  bnj121  30000  bnj130  30004  bnj605  30037  bnj581  30038  brpprod3b  30970  brapply  31021  brrestrict  31032  dfrdg4  31034  brsegle  31191  tendoset  34868  issubgr  40497  nbgrsym  40593  nb3grpr  40612  usgr2pthlem  40971  umgr2adedgwlk  41154  umgrwwlks2on  41163  elwspths2spth  41173  31wlkdlem8  41336  frgr3v  41447