Theorem 3anbi123i 1156

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3anbi1i  1158  3anbi2i  1159  3anbi3i  1160  syl3anb  1162  an33rean  1485  cadnot  1615  f13dfv  7294  poxp2  8168  xpord3lem  8174  poxp3  8175  xpord3pred  8177  axgroth5  10864  axgroth6  10868  hash7g  14525  cotr2g  15015  cbvprod  15949  cbvprodv  15950  prodeq1i  15952  isstruct  17189  pmtr3ncomlem1  19491  opprsubg  20352  addscut  28011  mulscut  28158  issubgr  29288  nbgrsym  29380  nb3grpr  29399  cplgr3v  29452  usgr2pthlem  29783  umgr2adedgwlk  29965  umgrwwlks2on  29977  elwspths2spth  29987  clwwlkccat  30009  clwlkclwwlk  30021  3wlkdlem8  30186  frgr3v  30294  or3dir  32479  unelldsys  34159  bnj156  34742  bnj206  34745  bnj887  34779  bnj121  34884  bnj130  34888  bnj605  34921  bnj581  34922  brpprod3b  35888  brapply  35939  brrestrict  35950  dfrdg4  35952  brsegle  36109  prodeq2si  36205  cbvprodvw2  36248  dfeqvrels3  38590  tendoset  40761  grtriproplem  47906  grtrif1o  47909  grlimgrtrilem1  47961  usgrexmpl2trifr  47996  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029