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 627	. . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
4		bi3.3	. . 3 ⊢ (𝜏 ↔ 𝜂)
5	3, 4	anbi12i 627	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜏) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
6		df-3an 1087	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜏))
7		df-3an 1087	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
8	5, 6, 7	3bitr4i 303	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  1480  cadnot  1609  f13dfv  7283  poxp2  8148  xpord3lem  8154  poxp3  8155  xpord3pred  8157  axgroth5  10848  axgroth6  10852  cotr2g  14956  cbvprod  15892  isstruct  17121  pmtr3ncomlem1  19428  opprsubg  20291  addscut  27908  mulscut  28045  issubgr  29097  nbgrsym  29189  nb3grpr  29208  cplgr3v  29261  usgr2pthlem  29590  umgr2adedgwlk  29769  umgrwwlks2on  29781  elwspths2spth  29791  clwwlkccat  29813  clwlkclwwlk  29825  3wlkdlem8  29990  frgr3v  30098  or3dir  32273  unelldsys  33777  bnj156  34359  bnj206  34362  bnj887  34396  bnj121  34501  bnj130  34505  bnj605  34538  bnj581  34539  brpprod3b  35483  brapply  35534  brrestrict  35545  dfrdg4  35547  brsegle  35704  dfeqvrels3  38061  tendoset  40232

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »