Theorem 3anbi2d 1435

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

Hypothesis

Ref	Expression
3anbi1d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
3anbi2d	⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏)))

Proof of Theorem 3anbi2d

Step	Hyp	Ref	Expression
1		biidd 264	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
2		3anbi1d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	3anbi12d 1431	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1082

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 209  df-an 399  df-3an 1084

This theorem is referenced by:  vtocl3gaf  3575  offval22  7775  ereq2  8289  wrdl3s3  14318  mhmlem  18211  isdrngrd  19520  lmodlema  19631  mdetunilem9  21221  neiptoptop  21731  neiptopnei  21732  hausnei  21928  regr1lem2  22340  ustuqtop4  22845  utopsnneiplem  22848  axtg5seg  26243  axtgupdim2  26249  axtgeucl  26250  brbtwn  26677  axlowdim  26739  axeuclidlem  26740  incistruhgr  26856  issubgr2  27046  wwlksnwwlksnon  27686  upgr4cycl4dv4e  27956  isnvlem  28379  csmdsymi  30103  br8d  30353  slmdlema  30824  carsgmon  31565  sitgclg  31593  tgoldbachgt  31927  axtgupdim2ALTV  31932  bnj852  32186  bnj18eq1  32192  bnj938  32202  bnj983  32216  bnj1318  32290  bnj1326  32291  cvmlift3lem4  32562  cvmlift3  32568  br8  32985  br6  32986  br4  32987  brcolinear2  33512  colineardim1  33515  brfs  33533  fscgr  33534  btwnconn1lem7  33547  brsegle  33562  unblimceq0  33839  sdclem2  35009  sdclem1  35010  sdc  35011  fdc  35012  cdleme18d  37423  cdlemk35s  38065  cdlemk39s  38067  monotoddzz  39530  jm2.27  39595  mendlmod  39783  fiiuncl  41317  wessf1ornlem  41434  fmulcl  41851  fmuldfeqlem1  41852  fprodcncf  42173  dvmptfprodlem  42218  dvmptfprod  42219  dvnprodlem2  42221  stoweidlem6  42281  stoweidlem8  42283  stoweidlem31  42306  stoweidlem34  42309  stoweidlem43  42318  stoweidlem52  42327  fourierdlem41  42423  fourierdlem48  42429  fourierdlem49  42430  ovnsubaddlem1  42842  ichexmpl2  43622  9gbo  43929  11gbo  43930  lmod1  44537