Theorem 3anbi123i 1155

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 627	. . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
4		bi3.3	. . 3 ⊢ (𝜏 ↔ 𝜂)
5	3, 4	anbi12i 627	. 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  1157  3anbi2i  1158  3anbi3i  1159  syl3anb  1161  an33rean  1483  cadnot  1612  f13dfv  7310  poxp2  8184  xpord3lem  8190  poxp3  8191  xpord3pred  8193  axgroth5  10893  axgroth6  10897  hash7g  14535  cotr2g  15025  cbvprod  15961  cbvprodv  15962  prodeq1i  15964  isstruct  17199  pmtr3ncomlem1  19515  opprsubg  20378  addscut  28029  mulscut  28176  issubgr  29306  nbgrsym  29398  nb3grpr  29417  cplgr3v  29470  usgr2pthlem  29799  umgr2adedgwlk  29978  umgrwwlks2on  29990  elwspths2spth  30000  clwwlkccat  30022  clwlkclwwlk  30034  3wlkdlem8  30199  frgr3v  30307  or3dir  32489  unelldsys  34122  bnj156  34704  bnj206  34707  bnj887  34741  bnj121  34846  bnj130  34850  bnj605  34883  bnj581  34884  brpprod3b  35851  brapply  35902  brrestrict  35913  dfrdg4  35915  brsegle  36072  prodeq2si  36168  cbvprodvw2  36213  dfeqvrels3  38545  tendoset  40716  grtriproplem  47790  grtrif1o  47793  grlimgrtrilem1  47818  usgrexmpl2trifr  47852