Theorem 3anbi2d 1353

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 245	. 2 |- ( ph -> ( th <-> th ) )
2		3anbi1d.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	3anbi12d 1349	1 |- ( ph -> ( ( th /\ ps /\ ta ) <-> ( th /\ ch /\ ta ) ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ w3a 991

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 190  df-an 377  df-3an 993

This theorem is referenced by:  vtocl3gaf  3128  offval22  6904  ereq2  7402  mhmlem  16861  isdrngrd  18056  lmodlema  18151  mdetunilem9  19700  neiptoptop  20202  neiptopnei  20203  hausnei  20399  regr1lem2  20810  ustuqtop4  21314  utopsnneiplem  21317  axtg5seg  24569  axtgupdim2  24575  axtgeucl  24576  brbtwn  24985  axlowdim  25047  axeuclidlem  25048  usgra2wlkspthlem1  25403  usgra2wlkspthlem2  25404  el2wlkonot  25653  el2spthonot  25654  el2spthonot0  25655  isnvlem  26285  csmdsymi  28043  br8d  28271  slmdlema  28570  carsgmon  29196  sitgclg  29225  axtgupdim2OLD  29535  bnj852  29782  bnj18eq1  29788  bnj938  29798  bnj983  29812  bnj1318  29884  bnj1326  29885  cvmlift3lem4  30095  cvmlift3  30101  br8  30446  br6  30447  br4  30448  brcolinear2  30875  colineardim1  30878  brfs  30896  fscgr  30897  btwnconn1lem7  30910  brsegle  30925  sdclem2  32117  sdclem1  32118  sdc  32119  fdc  32120  cdleme18d  33907  cdlemk35s  34550  cdlemk39s  34552  monotoddzz  35837  jm2.27  35909  mendlmod  36105  fiiuncl  37445  wessf1ornlem  37513  fmulcl  37745  fmuldfeqlem1  37746  fprodcncf  37865  dvmptfprodlem  37905  dvmptfprod  37906  dvnprodlem2  37908  stoweidlem6  37967  stoweidlem8  37969  stoweidlem31  37993  stoweidlem34  37996  stoweidlem43  38005  stoweidlem52  38014  fourierdlem41  38112  fourierdlem48  38119  fourierdlem49  38120  ovnsubaddlem1  38499  9gboa  39010  11gboa  39011  incistruhgr  39314  issubgr2  39490  upgr4cycl4dv4e  40022  lmod1  40654