Theorem 3anbi123i 1270

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

Syntax hints:   ↔ wb 196   ∧ wa 383   ∧ w3a 1054

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  3anbi1i  1272  3anbi2i  1273  3anbi3i  1274  syl3anb  1409  an33rean  1486  cadnot  1594  f13dfv  6570  axgroth5  9684  axgroth6  9688  cotr2g  13761  cbvprod  14689  isstruct  15917  pmtr3ncomlem1  17939  opprsubg  18682  issubgr  26208  nbgrsym  26308  nbgrsymOLD  26309  nb3grpr  26328  cplgr3v  26387  usgr2pthlem  26715  umgr2adedgwlk  26910  umgrwwlks2on  26923  elwspths2spth  26934  clwlkclwwlk  26968  clwlksfclwwlk  27049  3wlkdlem8  27145  frgr3v  27255  clwwlkccat  27332  or3dir  29436  unelldsys  30349  bnj156  30922  bnj206  30925  bnj887  30961  bnj121  31066  bnj130  31070  bnj605  31103  bnj581  31104  brpprod3b  32119  brapply  32170  brrestrict  32181  dfrdg4  32183  brsegle  32340  tendoset  36364