Theorem 3anbi2d 1304

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

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

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 975

This theorem is referenced by:  vtocl3gaf  3180  offval22  6859  ereq2  7316  isdrngrd  17205  lmodlema  17300  mdetunilem9  18889  neiptoptop  19398  neiptopnei  19399  hausnei  19595  regr1lem2  19976  ustuqtop4  20482  utopsnneiplem  20485  axtg5seg  23590  axtgupdim2  23597  axtgeucl  23598  brbtwn  23878  axlowdim  23940  axeuclidlem  23941  usgra2wlkspthlem1  24295  usgra2wlkspthlem2  24296  el2wlkonot  24545  el2spthonot  24546  el2spthonot0  24547  isnvlem  25179  csmdsymi  26929  br8d  27136  slmdlema  27408  sitgclg  27924  cvmlift3lem4  28407  cvmlift3  28413  br8  28762  br6  28763  br4  28764  brcolinear2  29285  colineardim1  29288  brfs  29306  fscgr  29307  btwnconn1lem7  29320  brsegle  29335  sdclem2  29838  sdclem1  29839  sdc  29840  fdc  29841  monotoddzz  30483  jm2.27  30554  mendlmod  30747  fmulcl  31131  fmuldfeqlem1  31132  stoweidlem6  31306  stoweidlem8  31308  stoweidlem31  31331  stoweidlem34  31334  stoweidlem43  31343  stoweidlem52  31352  fourierdlem41  31448  fourierdlem48  31455  fourierdlem49  31456  lmod1  32174  bnj852  33058  bnj18eq1  33064  bnj938  33074  bnj983  33088  bnj1318  33160  bnj1326  33161  cdleme18d  35091  cdlemk35s  35733  cdlemk39s  35735