Theorem 3anbi123i 1244

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

Syntax hints:   ↔ wb 195   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3anbi1i  1246  3anbi2i  1247  3anbi3i  1248  syl3anb  1361  an33rean  1438  cadnot  1545  f13dfv  6430  axgroth5  9525  axgroth6  9529  cotr2g  13563  cbvprod  14484  isstruct  15705  pmtr3ncomlem1  17716  opprsubg  18459  nb3grapr  25982  cusgra3v  25993  wwlknfi  26266  frgra3v  26529  or3dir  28692  unelldsys  29548  bnj156  30050  bnj206  30053  bnj887  30089  bnj121  30194  bnj130  30198  bnj605  30231  bnj581  30232  brpprod3b  31164  brapply  31215  brrestrict  31226  dfrdg4  31228  brsegle  31385  tendoset  35065  issubgr  40495  nbgrsym  40591  nb3grpr  40610  usgr2pthlem  40969  umgr2adedgwlk  41152  umgrwwlks2on  41161  elwspths2spth  41171  31wlkdlem8  41334  frgr3v  41445