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  6436  tfrlemi1  6478  tfr1onlemaccex  6494  tfrcllemaccex  6507  ereq1  6687  updjud  7249  ctssdclemr  7279  tapeq1  7438  tapeq2  7439  elinp  7661  sup3exmid  9104  iccshftr  10190  iccshftl  10192  iccdil  10194  icccntr  10196  fzaddel  10255  elfzomelpfzo  10437  seq3f1olemstep  10736  seq3f1olemp  10737  wrdl1s1  11163  sumeq1  11866  summodclem2  11893  summodc  11894  zsumdc  11895  prodmodclem2  12088  prodmodc  12089  divalglemnn  12429  divalglemeunn  12432  divalglemeuneg  12434  dfgcd2  12535  pythagtriplem18  12804  pythagtriplem19  12805  ctiunct  13011  ssomct  13016  isstruct2im  13042  isstruct2r  13043  ptex  13297  imasmnd2  13485  imasgrp2  13647  isrngd  13916  imasrng  13919  isringd  14004  imasring  14027  subrngpropd  14180  issubrg3  14211  islmod  14255  lmodlema  14256  islmodd  14257  lmodprop2d  14312  fiinopn  14678  lmfval  14867  upxp  14946  ivthdich  15327  2irrexpqap  15652  wksfval  16035  iswlk  16036  dceqnconst  16428  dcapnconst  16429