Theorem 3anbi2d 1303

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 1299	1 |- ( ph -> ( ( th /\ ps /\ ta ) <-> ( th /\ ch /\ ta ) ) )

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

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 974

This theorem is referenced by:  vtocl3gaf  3160  offval22  6861  ereq2  7318  mhmlem  16061  isdrngrd  17293  lmodlema  17388  mdetunilem9  18992  neiptoptop  19502  neiptopnei  19503  hausnei  19699  regr1lem2  20111  ustuqtop4  20617  utopsnneiplem  20620  axtg5seg  23731  axtgupdim2  23738  axtgeucl  23739  brbtwn  24071  axlowdim  24133  axeuclidlem  24134  usgra2wlkspthlem1  24488  usgra2wlkspthlem2  24489  el2wlkonot  24738  el2spthonot  24739  el2spthonot0  24740  isnvlem  25372  csmdsymi  27122  br8d  27332  slmdlema  27616  sitgclg  28154  cvmlift3lem4  28637  cvmlift3  28643  br8  29157  br6  29158  br4  29159  brcolinear2  29680  colineardim1  29683  brfs  29701  fscgr  29702  btwnconn1lem7  29715  brsegle  29730  sdclem2  30207  sdclem1  30208  sdc  30209  fdc  30210  monotoddzz  30851  jm2.27  30922  mendlmod  31115  fmulcl  31503  fmuldfeqlem1  31504  stoweidlem6  31677  stoweidlem8  31679  stoweidlem31  31702  stoweidlem34  31705  stoweidlem43  31714  stoweidlem52  31723  fourierdlem41  31819  fourierdlem48  31826  fourierdlem49  31827  lmod1  32823  bnj852  33707  bnj18eq1  33713  bnj938  33723  bnj983  33737  bnj1318  33809  bnj1326  33810  cdleme18d  35743  cdlemk35s  36386  cdlemk39s  36388