Theorem 3anbi123d 1349

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

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 1007

This theorem is referenced by:  3anbi12d  1350  3anbi13d  1351  3anbi23d  1352  limeq  4480  smoeq  6499  tfrlemi1  6541  tfr1onlemaccex  6557  tfrcllemaccex  6570  ereq1  6752  updjud  7341  ctssdclemr  7371  tapeq1  7531  tapeq2  7532  elinp  7754  sup3exmid  9196  iccshftr  10290  iccshftl  10292  iccdil  10294  icccntr  10296  fzaddel  10356  elfzomelpfzo  10539  seq3f1olemstep  10839  seq3f1olemp  10840  wrdl1s1  11273  sumeq1  11995  summodclem2  12023  summodc  12024  zsumdc  12025  prodmodclem2  12218  prodmodc  12219  divalglemnn  12559  divalglemeunn  12562  divalglemeuneg  12564  dfgcd2  12665  pythagtriplem18  12934  pythagtriplem19  12935  ctiunct  13141  ssomct  13146  isstruct2im  13172  isstruct2r  13173  ptex  13427  imasmnd2  13615  imasgrp2  13777  isrngd  14047  imasrng  14050  isringd  14135  imasring  14158  subrngpropd  14311  issubrg3  14342  islmod  14387  lmodlema  14388  islmodd  14389  lmodprop2d  14444  fiinopn  14815  lmfval  15004  upxp  15083  ivthdich  15464  2irrexpqap  15789  issubgr  16198  wksfval  16263  iswlk  16264  isclwwlk  16335  clwwlkn1loopb  16361  s2elclwwlknon2  16377  3dom  16708  dceqnconst  16793  dcapnconst  16794