Theorem 3anbi123d 1325

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 473	. . 3 |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ ta ) ) )
4		bi3d.3	. . 3 |- ( ph -> ( et <-> ze ) )
5	3, 4	anbi12d 473	. 2 |- ( ph -> ( ( ( ps /\ th ) /\ et ) <-> ( ( ch /\ ta ) /\ ze ) ) )
6		df-3an 983	. 2 |- ( ( ps /\ th /\ et ) <-> ( ( ps /\ th ) /\ et ) )
7		df-3an 983	. 2 |- ( ( ch /\ ta /\ ze ) <-> ( ( ch /\ ta ) /\ ze ) )
8	5, 6, 7	3bitr4g 223	1 |- ( ph -> ( ( ps /\ th /\ et ) <-> ( ch /\ ta /\ ze ) ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 981

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

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  3anbi12d  1326  3anbi13d  1327  3anbi23d  1328  limeq  4424  smoeq  6376  tfrlemi1  6418  tfr1onlemaccex  6434  tfrcllemaccex  6447  ereq1  6627  updjud  7184  ctssdclemr  7214  tapeq1  7364  tapeq2  7365  elinp  7587  sup3exmid  9030  iccshftr  10116  iccshftl  10118  iccdil  10120  icccntr  10122  fzaddel  10181  elfzomelpfzo  10360  seq3f1olemstep  10659  seq3f1olemp  10660  wrdl1s1  11084  sumeq1  11666  summodclem2  11693  summodc  11694  zsumdc  11695  prodmodclem2  11888  prodmodc  11889  divalglemnn  12229  divalglemeunn  12232  divalglemeuneg  12234  dfgcd2  12335  pythagtriplem18  12604  pythagtriplem19  12605  ctiunct  12811  ssomct  12816  isstruct2im  12842  isstruct2r  12843  ptex  13096  imasmnd2  13284  imasgrp2  13446  isrngd  13715  imasrng  13718  isringd  13803  imasring  13826  subrngpropd  13978  issubrg3  14009  islmod  14053  lmodlema  14054  islmodd  14055  lmodprop2d  14110  fiinopn  14476  lmfval  14664  upxp  14744  ivthdich  15125  2irrexpqap  15450  dceqnconst  16003  dcapnconst  16004