Theorem 3anbi2d 1294

Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)

Hypothesis

Ref	Expression
3anbi1d.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
3anbi2d	|- ( ph -> ( ( th /\ ps /\ ta ) <-> ( th /\ ch /\ ta ) ) )

Proof of Theorem 3anbi2d

Step	Hyp	Ref	Expression
1		biidd 237	. 2 |- ( ph -> ( th <-> th ) )
2		3anbi1d.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	3anbi12d 1290	1 |- ( ph -> ( ( th /\ ps /\ ta ) <-> ( th /\ ch /\ ta ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ w3a 965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967

This theorem is referenced by:  vtocl3gaf  3034  offval22  6647  ereq2  7101  isdrngrd  16836  lmodlema  16931  mdetunilem9  18401  neiptoptop  18710  neiptopnei  18711  hausnei  18907  regr1lem2  19288  ustuqtop4  19794  utopsnneiplem  19797  axtg5seg  22901  axtgupdim2  22907  axtgeucl  22908  brbtwn  23096  axlowdim  23158  axeuclidlem  23159  isnvlem  23939  csmdsymi  25689  br8d  25893  slmdlema  26170  sitgclg  26680  cvmlift3lem4  27163  cvmlift3  27169  br8  27517  br6  27518  br4  27519  brcolinear2  28040  colineardim1  28043  brfs  28061  fscgr  28062  btwnconn1lem7  28075  brsegle  28090  sdclem2  28591  sdclem1  28592  sdc  28593  fdc  28594  monotoddzz  29237  jm2.27  29310  mendlmod  29503  fmulcl  29715  fmuldfeqlem1  29716  stoweidlem6  29754  stoweidlem8  29756  stoweidlem31  29779  stoweidlem34  29782  stoweidlem43  29791  stoweidlem52  29800  usgra2wlkspthlem1  30249  usgra2wlkspthlem2  30250  el2wlkonot  30341  el2spthonot  30342  el2spthonot0  30343  lmod1  30923  bnj852  31801  bnj18eq1  31807  bnj938  31817  bnj983  31831  bnj1318  31903  bnj1326  31904  cdleme18d  33779  cdlemk35s  34421  cdlemk39s  34423