Theorem 3anbi123i 1251

Description: Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.)

Hypotheses

Ref	Expression
bi3.1	|- ( ph <-> ps )
bi3.2	|- ( ch <-> th )
bi3.3	|- ( ta <-> et )

Assertion

Ref	Expression
3anbi123i	|- ( ( ph /\ ch /\ ta ) <-> ( ps /\ th /\ et ) )

Proof of Theorem 3anbi123i

Step	Hyp	Ref	Expression
1		bi3.1	. . . 4 |- ( ph <-> ps )
2		bi3.2	. . . 4 |- ( ch <-> th )
3	1, 2	anbi12i 733	. . 3 |- ( ( ph /\ ch ) <-> ( ps /\ th ) )
4		bi3.3	. . 3 |- ( ta <-> et )
5	3, 4	anbi12i 733	. 2 |- ( ( ( ph /\ ch ) /\ ta ) <-> ( ( ps /\ th ) /\ et ) )
6		df-3an 1039	. 2 |- ( ( ph /\ ch /\ ta ) <-> ( ( ph /\ ch ) /\ ta ) )
7		df-3an 1039	. 2 |- ( ( ps /\ th /\ et ) <-> ( ( ps /\ th ) /\ et ) )
8	5, 6, 7	3bitr4i 292	1 |- ( ( ph /\ ch /\ ta ) <-> ( ps /\ th /\ et ) )

Syntax hints:   <-> wb 196   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3anbi1i  1253  3anbi2i  1254  3anbi3i  1255  syl3anb  1369  an33rean  1446  cadnot  1554  f13dfv  6530  axgroth5  9646  axgroth6  9650  cotr2g  13715  cbvprod  14645  isstruct  15870  pmtr3ncomlem1  17893  opprsubg  18636  issubgr  26163  nbgrsym  26265  nb3grpr  26284  usgr2pthlem  26659  umgr2adedgwlk  26841  umgrwwlks2on  26850  elwspths2spth  26862  clwlkclwwlk  26903  clwlksfclwwlk  26962  3wlkdlem8  27027  frgr3v  27139  or3dir  29308  unelldsys  30221  bnj156  30796  bnj206  30799  bnj887  30835  bnj121  30940  bnj130  30944  bnj605  30977  bnj581  30978  brpprod3b  31994  brapply  32045  brrestrict  32056  dfrdg4  32058  brsegle  32215  tendoset  36047