Theorem 3anbi2d 1443

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 262	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
2		3anbi1d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	3anbi12d 1439	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  vtocl3gafOLD  3548  vtocl3gaOLD  3550  offval22  8067  ereq2  8679  brttrcl  9666  ttrclss  9673  ttrclselem2  9679  wrdl3s3  14928  mhmlem  18994  isdrngrd  20675  isdrngrdOLD  20677  lmodlema  20771  mdetunilem9  22507  neiptoptop  23018  neiptopnei  23019  hausnei  23215  regr1lem2  23627  ustuqtop4  24132  utopsnneiplem  24135  axtg5seg  28392  axtgupdim2  28398  axtgeucl  28399  brbtwn  28826  axlowdim  28888  axeuclidlem  28889  incistruhgr  29006  issubgr2  29199  wwlksnwwlksnon  29845  upgr4cycl4dv4e  30114  isnvlem  30539  csmdsymi  32263  br8d  32538  slmdlema  33156  constrconj  33735  constrllcllem  33742  constrcccllem  33744  constrcbvlem  33745  carsgmon  34305  sitgclg  34333  tgoldbachgt  34654  axtgupdim2ALTV  34659  bnj852  34911  bnj18eq1  34917  bnj938  34927  bnj983  34941  bnj1318  35015  bnj1326  35016  cvmlift3lem4  35309  cvmlift3  35315  br8  35743  br6  35744  br4  35745  brcolinear2  36046  colineardim1  36049  brfs  36067  fscgr  36068  btwnconn1lem7  36081  brsegle  36096  unblimceq0  36495  sdclem2  37736  sdclem1  37737  sdc  37738  fdc  37739  cdleme18d  40289  cdlemk35s  40931  cdlemk39s  40933  monotoddzz  42932  jm2.27  42997  mendlmod  43178  minregex2  43524  fiiuncl  45059  wessf1ornlem  45179  fmulcl  45579  fmuldfeqlem1  45580  fprodcncf  45898  dvmptfprodlem  45942  dvmptfprod  45943  dvnprodlem2  45945  stoweidlem6  46004  stoweidlem8  46006  stoweidlem31  46029  stoweidlem34  46032  stoweidlem43  46041  stoweidlem52  46050  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  ovnsubaddlem1  46568  ichexmpl2  47471  9gbo  47775  11gbo  47776  lmod1  48481  cnelsubclem  49592