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  4425  smoeq  6378  tfrlemi1  6420  tfr1onlemaccex  6436  tfrcllemaccex  6449  ereq1  6629  updjud  7186  ctssdclemr  7216  tapeq1  7366  tapeq2  7367  elinp  7589  sup3exmid  9032  iccshftr  10118  iccshftl  10120  iccdil  10122  icccntr  10124  fzaddel  10183  elfzomelpfzo  10362  seq3f1olemstep  10661  seq3f1olemp  10662  wrdl1s1  11087  sumeq1  11699  summodclem2  11726  summodc  11727  zsumdc  11728  prodmodclem2  11921  prodmodc  11922  divalglemnn  12262  divalglemeunn  12265  divalglemeuneg  12267  dfgcd2  12368  pythagtriplem18  12637  pythagtriplem19  12638  ctiunct  12844  ssomct  12849  isstruct2im  12875  isstruct2r  12876  ptex  13129  imasmnd2  13317  imasgrp2  13479  isrngd  13748  imasrng  13751  isringd  13836  imasring  13859  subrngpropd  14011  issubrg3  14042  islmod  14086  lmodlema  14087  islmodd  14088  lmodprop2d  14143  fiinopn  14509  lmfval  14697  upxp  14777  ivthdich  15158  2irrexpqap  15483  dceqnconst  16036  dcapnconst  16037