Theorem 3anbi123i 1153

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

Syntax hints:   ↔ wb 205   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  3anbi1i  1155  3anbi2i  1156  3anbi3i  1157  syl3anb  1159  an33rean  1481  an33reanOLD  1482  cadnot  1618  f13dfv  7127  axgroth5  10511  axgroth6  10515  cotr2g  14615  cbvprod  15553  isstruct  16781  pmtr3ncomlem1  18996  opprsubg  19793  issubgr  27541  nbgrsym  27633  nb3grpr  27652  cplgr3v  27705  usgr2pthlem  28032  umgr2adedgwlk  28211  umgrwwlks2on  28223  elwspths2spth  28233  clwwlkccat  28255  clwlkclwwlk  28267  3wlkdlem8  28432  frgr3v  28540  or3dir  30712  unelldsys  32026  bnj156  32607  bnj206  32610  bnj887  32645  bnj121  32750  bnj130  32754  bnj605  32787  bnj581  32788  poxp2  33717  xpord3lem  33722  poxp3  33723  brpprod3b  34116  brapply  34167  brrestrict  34178  dfrdg4  34180  brsegle  34337  dfeqvrels3  36629  tendoset  38700