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 629	. . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
4		bi3.3	. . 3 ⊢ (𝜏 ↔ 𝜂)
5	3, 4	anbi12i 629	. 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  1486  cadnot  1617  f13dfv  7224  poxp2  8088  xpord3lem  8094  poxp3  8095  xpord3pred  8097  axgroth5  10742  axgroth6  10746  hash7g  14443  cotr2g  14933  cbvprod  15873  cbvprodv  15874  prodeq1i  15876  isstruct  17117  pmtr3ncomlem1  19443  opprsubg  20327  addcuts  27988  mulcut  28142  ons2ind  28285  issubgr  29358  nbgrsym  29450  nb3grpr  29469  cplgr3v  29522  usgr2pthlem  29850  umgr2adedgwlk  30032  usgrwwlks2on  30045  umgrwwlks2on  30046  elwspths2spth  30057  clwwlkccat  30079  clwlkclwwlk  30091  3wlkdlem8  30256  frgr3v  30364  or3dir  32548  unelldsys  34322  bnj156  34891  bnj206  34894  bnj887  34928  bnj121  35032  bnj130  35036  bnj605  35069  bnj581  35070  brpprod3b  36087  brapply  36138  brrestrict  36151  dfrdg4  36153  brsegle  36310  prodeq2si  36406  cbvprodvw2  36449  dfeqvrels3  39012  tendoset  41223  grtriproplem  48431  grtrif1o  48434  usgrexmpl2trifr  48529  gpg5nbgrvtx03starlem1  48560  gpg5nbgrvtx03starlem2  48561  gpg5nbgrvtx03starlem3  48562  gpg5nbgrvtx13starlem1  48563  gpg5nbgrvtx13starlem2  48564  gpg5nbgrvtx13starlem3  48565  gpg5edgnedg  48622  2arwcatlem1  50086  setc1onsubc  50093