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  3561  vtocl3gaOLD  3563  offval22  8087  ereq2  8727  brttrcl  9727  ttrclss  9734  ttrclselem2  9740  wrdl3s3  14981  mhmlem  19045  isdrngrd  20726  isdrngrdOLD  20728  lmodlema  20822  mdetunilem9  22558  neiptoptop  23069  neiptopnei  23070  hausnei  23266  regr1lem2  23678  ustuqtop4  24183  utopsnneiplem  24186  axtg5seg  28444  axtgupdim2  28450  axtgeucl  28451  brbtwn  28878  axlowdim  28940  axeuclidlem  28941  incistruhgr  29058  issubgr2  29251  wwlksnwwlksnon  29897  upgr4cycl4dv4e  30166  isnvlem  30591  csmdsymi  32315  br8d  32590  slmdlema  33200  constrconj  33779  constrllcllem  33786  constrcccllem  33788  constrcbvlem  33789  carsgmon  34346  sitgclg  34374  tgoldbachgt  34695  axtgupdim2ALTV  34700  bnj852  34952  bnj18eq1  34958  bnj938  34968  bnj983  34982  bnj1318  35056  bnj1326  35057  cvmlift3lem4  35344  cvmlift3  35350  br8  35773  br6  35774  br4  35775  brcolinear2  36076  colineardim1  36079  brfs  36097  fscgr  36098  btwnconn1lem7  36111  brsegle  36126  unblimceq0  36525  sdclem2  37766  sdclem1  37767  sdc  37768  fdc  37769  cdleme18d  40314  cdlemk35s  40956  cdlemk39s  40958  monotoddzz  42967  jm2.27  43032  mendlmod  43213  minregex2  43559  fiiuncl  45089  wessf1ornlem  45209  fmulcl  45610  fmuldfeqlem1  45611  fprodcncf  45929  dvmptfprodlem  45973  dvmptfprod  45974  dvnprodlem2  45976  stoweidlem6  46035  stoweidlem8  46037  stoweidlem31  46060  stoweidlem34  46063  stoweidlem43  46072  stoweidlem52  46081  fourierdlem41  46177  fourierdlem48  46183  fourierdlem49  46184  ovnsubaddlem1  46599  ichexmpl2  47484  9gbo  47788  11gbo  47789  lmod1  48468  cnelsubclem  49480