Theorem 3anbi2d 1440

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 1436	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  3582  vtocl3gaOLD  3584  offval22  8112  ereq2  8752  brttrcl  9751  ttrclss  9758  ttrclselem2  9764  wrdl3s3  14998  mhmlem  19093  isdrngrd  20783  isdrngrdOLD  20785  lmodlema  20880  mdetunilem9  22642  neiptoptop  23155  neiptopnei  23156  hausnei  23352  regr1lem2  23764  ustuqtop4  24269  utopsnneiplem  24272  axtg5seg  28488  axtgupdim2  28494  axtgeucl  28495  brbtwn  28929  axlowdim  28991  axeuclidlem  28992  incistruhgr  29111  issubgr2  29304  wwlksnwwlksnon  29945  upgr4cycl4dv4e  30214  isnvlem  30639  csmdsymi  32363  br8d  32630  slmdlema  33192  constrconj  33750  carsgmon  34296  sitgclg  34324  tgoldbachgt  34657  axtgupdim2ALTV  34662  bnj852  34914  bnj18eq1  34920  bnj938  34930  bnj983  34944  bnj1318  35018  bnj1326  35019  cvmlift3lem4  35307  cvmlift3  35313  br8  35736  br6  35737  br4  35738  brcolinear2  36040  colineardim1  36043  brfs  36061  fscgr  36062  btwnconn1lem7  36075  brsegle  36090  unblimceq0  36490  sdclem2  37729  sdclem1  37730  sdc  37731  fdc  37732  cdleme18d  40278  cdlemk35s  40920  cdlemk39s  40922  monotoddzz  42932  jm2.27  42997  mendlmod  43178  minregex2  43525  fiiuncl  45005  wessf1ornlem  45128  fmulcl  45537  fmuldfeqlem1  45538  fprodcncf  45856  dvmptfprodlem  45900  dvmptfprod  45901  dvnprodlem2  45903  stoweidlem6  45962  stoweidlem8  45964  stoweidlem31  45987  stoweidlem34  45990  stoweidlem43  45999  stoweidlem52  46008  fourierdlem41  46104  fourierdlem48  46110  fourierdlem49  46111  ovnsubaddlem1  46526  ichexmpl2  47395  9gbo  47699  11gbo  47700  lmod1  48338