Theorem 3anbi2d 1469

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  offval22  8085  ereq2  8705  brttrcl  9692  ttrclss  9699  ttrclselem2  9705  wrdl3s3  15035  mhmlem  19185  isdrngrd  20932  isdrngrdOLD  20934  lmodlema  21049  mdetunilem9  22842  neiptoptop  23356  neiptopnei  23357  hausnei  23553  regr1lem2  23966  ustuqtop4  24470  utopsnneiplem  24473  bdayfinbndlem1  28732  axtg5seg  28806  axtgupdim2  28812  axtgeucl  28813  brbtwn  29356  axlowdim  29418  axeuclidlem  29419  incistruhgr  29536  issubgr2  29732  wwlksnwwlksnon  30383  upgr4cycl4dv4e  30665  isnvlem  31091  csmdsymi  32815  br8d  33081  slmdlema  33643  constrconj  34255  constrllcllem  34262  constrcccllem  34264  constrcbvlem  34265  carsgmon  34825  sitgclg  34853  tgoldbachgt  35171  axtgupdim2ALTV  35176  bnj852  35430  bnj18eq1  35436  bnj938  35446  bnj983  35460  bnj1318  35534  bnj1326  35535  cvmlift3lem4  35901  cvmlift3  35907  br8  36335  br6  36336  br4  36337  brcolinear2  36638  colineardim1  36641  brfs  36659  fscgr  36660  btwnconn1lem7  36673  brsegle  36688  unblimceq0  37204  sdclem2  38492  sdclem1  38493  sdc  38494  fdc  38495  cdleme18d  41168  cdlemk35s  41810  cdlemk39s  41812  monotoddzz  43784  jm2.27  43849  mendlmod  44030  minregex2  44375  fiiuncl  45899  wessf1ornlem  46017  fmulcl  46411  fmuldfeqlem1  46412  fprodcncf  46728  dvmptfprodlem  46772  dvmptfprod  46773  dvnprodlem2  46775  stoweidlem6  46834  stoweidlem8  46836  stoweidlem31  46859  stoweidlem34  46862  stoweidlem43  46871  stoweidlem52  46880  fourierdlem41  46976  fourierdlem48  46982  fourierdlem49  46983  ovnsubaddlem1  47398  ichexmpl2  48370  9gbo  48690  11gbo  48691  lmod1  49422  cnelsubclem  50529