Theorem 3anbi123d 1346

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 1004	. 2 |- ( ( ps /\ th /\ et ) <-> ( ( ps /\ th ) /\ et ) )
7		df-3an 1004	. 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 1002

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 1004

This theorem is referenced by:  3anbi12d  1347  3anbi13d  1348  3anbi23d  1349  limeq  4468  smoeq  6442  tfrlemi1  6484  tfr1onlemaccex  6500  tfrcllemaccex  6513  ereq1  6695  updjud  7257  ctssdclemr  7287  tapeq1  7446  tapeq2  7447  elinp  7669  sup3exmid  9112  iccshftr  10198  iccshftl  10200  iccdil  10202  icccntr  10204  fzaddel  10263  elfzomelpfzo  10445  seq3f1olemstep  10744  seq3f1olemp  10745  wrdl1s1  11171  sumeq1  11874  summodclem2  11901  summodc  11902  zsumdc  11903  prodmodclem2  12096  prodmodc  12097  divalglemnn  12437  divalglemeunn  12440  divalglemeuneg  12442  dfgcd2  12543  pythagtriplem18  12812  pythagtriplem19  12813  ctiunct  13019  ssomct  13024  isstruct2im  13050  isstruct2r  13051  ptex  13305  imasmnd2  13493  imasgrp2  13655  isrngd  13924  imasrng  13927  isringd  14012  imasring  14035  subrngpropd  14188  issubrg3  14219  islmod  14263  lmodlema  14264  islmodd  14265  lmodprop2d  14320  fiinopn  14686  lmfval  14875  upxp  14954  ivthdich  15335  2irrexpqap  15660  wksfval  16043  iswlk  16044  3dom  16381  dceqnconst  16458  dcapnconst  16459