Theorem 3anbi123d 1290

Description: Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.)

Hypotheses

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

Assertion

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

Proof of Theorem 3anbi123d

Step	Hyp	Ref	Expression
1		bi3d.1	. . . 4 |- ( ph -> ( ps <-> ch ) )
2		bi3d.2	. . . 4 |- ( ph -> ( th <-> ta ) )
3	1, 2	anbi12d 464	. . 3 |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ ta ) ) )
4		bi3d.3	. . 3 |- ( ph -> ( et <-> ze ) )
5	3, 4	anbi12d 464	. 2 |- ( ph -> ( ( ( ps /\ th ) /\ et ) <-> ( ( ch /\ ta ) /\ ze ) ) )
6		df-3an 964	. 2 |- ( ( ps /\ th /\ et ) <-> ( ( ps /\ th ) /\ et ) )
7		df-3an 964	. 2 |- ( ( ch /\ ta /\ ze ) <-> ( ( ch /\ ta ) /\ ze ) )
8	5, 6, 7	3bitr4g 222	1 |- ( ph -> ( ( ps /\ th /\ et ) <-> ( ch /\ ta /\ ze ) ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   /\ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  3anbi12d  1291  3anbi13d  1292  3anbi23d  1293  limeq  4299  smoeq  6187  tfrlemi1  6229  tfr1onlemaccex  6245  tfrcllemaccex  6258  ereq1  6436  updjud  6967  ctssdclemr  6997  elinp  7282  sup3exmid  8715  iccshftr  9777  iccshftl  9779  iccdil  9781  icccntr  9783  fzaddel  9839  elfzomelpfzo  10008  seq3f1olemstep  10274  seq3f1olemp  10275  sumeq1  11124  summodclem2  11151  summodc  11152  zsumdc  11153  prodmodclem2  11346  prodmodc  11347  divalglemnn  11615  divalglemeunn  11618  divalglemeuneg  11620  dfgcd2  11702  ctiunct  11953  isstruct2im  11969  isstruct2r  11970  fiinopn  12171  lmfval  12361  upxp  12441