Theorem 3anbi123d 1323

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

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 982

This theorem is referenced by:  3anbi12d  1324  3anbi13d  1325  3anbi23d  1326  limeq  4408  smoeq  6343  tfrlemi1  6385  tfr1onlemaccex  6401  tfrcllemaccex  6414  ereq1  6594  updjud  7141  ctssdclemr  7171  tapeq1  7312  tapeq2  7313  elinp  7534  sup3exmid  8976  iccshftr  10060  iccshftl  10062  iccdil  10064  icccntr  10066  fzaddel  10125  elfzomelpfzo  10298  seq3f1olemstep  10585  seq3f1olemp  10586  sumeq1  11498  summodclem2  11525  summodc  11526  zsumdc  11527  prodmodclem2  11720  prodmodc  11721  divalglemnn  12059  divalglemeunn  12062  divalglemeuneg  12064  dfgcd2  12151  pythagtriplem18  12419  pythagtriplem19  12420  ctiunct  12597  ssomct  12602  isstruct2im  12628  isstruct2r  12629  ptex  12875  imasgrp2  13180  isrngd  13449  imasrng  13452  isringd  13537  imasring  13560  subrngpropd  13712  issubrg3  13743  islmod  13787  lmodlema  13788  islmodd  13789  lmodprop2d  13844  fiinopn  14172  lmfval  14360  upxp  14440  ivthdich  14807  2irrexpqap  15110  dceqnconst  15550  dcapnconst  15551