Theorem 3anbi2d 1295

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 1291	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  3138  offval22  6755  ereq2  7212  isdrngrd  16973  lmodlema  17068  mdetunilem9  18551  neiptoptop  18860  neiptopnei  18861  hausnei  19057  regr1lem2  19438  ustuqtop4  19944  utopsnneiplem  19947  axtg5seg  23052  axtgupdim2  23059  axtgeucl  23060  brbtwn  23290  axlowdim  23352  axeuclidlem  23353  isnvlem  24133  csmdsymi  25883  br8d  26086  slmdlema  26357  sitgclg  26865  cvmlift3lem4  27348  cvmlift3  27354  br8  27703  br6  27704  br4  27705  brcolinear2  28226  colineardim1  28229  brfs  28247  fscgr  28248  btwnconn1lem7  28261  brsegle  28276  sdclem2  28779  sdclem1  28780  sdc  28781  fdc  28782  monotoddzz  29425  jm2.27  29498  mendlmod  29691  fmulcl  29903  fmuldfeqlem1  29904  stoweidlem6  29942  stoweidlem8  29944  stoweidlem31  29967  stoweidlem34  29970  stoweidlem43  29979  stoweidlem52  29988  usgra2wlkspthlem1  30437  usgra2wlkspthlem2  30438  el2wlkonot  30529  el2spthonot  30530  el2spthonot0  30531  lmod1  31144  bnj852  32217  bnj18eq1  32223  bnj938  32233  bnj983  32247  bnj1318  32319  bnj1326  32320  cdleme18d  34248  cdlemk35s  34890  cdlemk39s  34892