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  cadnot  1612  f13dfv  7025  axgroth5  10240  axgroth6  10244  cotr2g  14330  cbvprod  15263  isstruct  16490  pmtr3ncomlem1  18595  opprsubg  19380  issubgr  27047  nbgrsym  27139  nb3grpr  27158  cplgr3v  27211  usgr2pthlem  27538  umgr2adedgwlk  27718  umgrwwlks2on  27730  elwspths2spth  27740  clwwlkccat  27762  clwlkclwwlk  27774  3wlkdlem8  27940  frgr3v  28048  or3dir  30220  unelldsys  31412  bnj156  31993  bnj206  31996  bnj887  32031  bnj121  32137  bnj130  32141  bnj605  32174  bnj581  32175  brpprod3b  33343  brapply  33394  brrestrict  33405  dfrdg4  33407  brsegle  33564  dfeqvrels3  35818  tendoset  37889