Theorem 3anbi2d 1462

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 1458	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏)))

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

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 400  df-3an 1100

This theorem is referenced by:  offval22  8067  ereq2  8687  brttrcl  9668  ttrclss  9675  ttrclselem2  9681  wrdl3s3  14975  mhmlem  19104  isdrngrd  20812  isdrngrdOLD  20814  lmodlema  20929  mdetunilem9  22677  neiptoptop  23188  neiptopnei  23189  hausnei  23385  regr1lem2  23797  ustuqtop4  24301  utopsnneiplem  24304  bdayfinbndlem1  28557  axtg5seg  28631  axtgupdim2  28637  axtgeucl  28638  brbtwn  29097  axlowdim  29159  axeuclidlem  29160  incistruhgr  29277  issubgr2  29470  wwlksnwwlksnon  30112  upgr4cycl4dv4e  30384  isnvlem  30810  csmdsymi  32534  br8d  32807  slmdlema  33380  constrconj  34039  constrllcllem  34046  constrcccllem  34048  constrcbvlem  34049  carsgmon  34608  sitgclg  34636  tgoldbachgt  34954  axtgupdim2ALTV  34959  bnj852  35213  bnj18eq1  35219  bnj938  35229  bnj983  35243  bnj1318  35317  bnj1326  35318  cvmlift3lem4  35669  cvmlift3  35675  br8  36103  br6  36104  br4  36105  brcolinear2  36405  colineardim1  36408  brfs  36426  fscgr  36427  btwnconn1lem7  36440  brsegle  36455  unblimceq0  36942  sdclem2  38238  sdclem1  38239  sdc  38240  fdc  38241  cdleme18d  40916  cdlemk35s  41558  cdlemk39s  41560  monotoddzz  43517  jm2.27  43582  mendlmod  43763  minregex2  44108  fiiuncl  45642  wessf1ornlem  45760  fmulcl  46154  fmuldfeqlem1  46155  fprodcncf  46471  dvmptfprodlem  46515  dvmptfprod  46516  dvnprodlem2  46518  stoweidlem6  46577  stoweidlem8  46579  stoweidlem31  46602  stoweidlem34  46605  stoweidlem43  46614  stoweidlem52  46623  fourierdlem41  46719  fourierdlem48  46725  fourierdlem49  46726  ovnsubaddlem1  47141  ichexmpl2  48073  9gbo  48393  11gbo  48394  lmod1  49111  cnelsubclem  50221