Theorem 3anbi3d 1470

Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)

Hypothesis

Ref	Expression
3anbi1d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
3anbi3d	⊢ (𝜑 → ((𝜃 ∧ 𝜏 ∧ 𝜓) ↔ (𝜃 ∧ 𝜏 ∧ 𝜒)))

Proof of Theorem 3anbi3d

Step	Hyp	Ref	Expression
1		biidd 265	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
2		3anbi1d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	3anbi13d 1466	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:  ceqsex3v  3502  ceqsex4v  3503  ceqsex8v  3505  mob  3674  offval22  8103  smogt  8382  ttrcleq  9717  cfsmolem  10355  fseq1m1p1  13740  pfxsuff1eqwrdeq  14856  2swrd2eqwrdeq  15115  wrdl3s3  15124  prodmo  16112  fprod  16117  divalg  16582  funcres2b  18081  posi  18500  mhmlem  19281  isdrngrd  21032  isdrngrdOLD  21034  lmodlema  21149  connsub  23748  lmmbr3  25590  lmmcvg  25591  dvmptfsum  26304  nosupprefixmo  28066  noinfprefixmo  28067  nosupcbv  28068  nosupno  28069  nosupfv  28072  noinfcbv  28083  noinfno  28084  noinffv  28087  bdayfinbndlem2  28863  axtg5seg  28936  axtgupdim2  28942  axtgeucl  28943  ishlg2  29074  ishlg  29077  hlcomb  29078  brbtwn  29486  axlowdim  29548  axeuclidlem  29549  usgr2wlkspth  30354  usgr2pth0  30360  wwlksnwwlksnon  30513  usgrwwlks2on  30556  umgrwwlks2on  30557  upgr3v3e3cycl  30790  upgr4cycl4dv4e  30795  nvi  31225  isslmd  33813  slmdlema  33814  opprlidlabs  34059  constrcccllem  34436  constrcbvlem  34437  inelsros  34861  diffiunisros  34862  hgt749d  35328  tgoldbachgt  35342  axtgupdim2ALTV  35347  afsval  35353  brafs  35354  bnj981  35630  bnj1326  35706  cvmlift3lem2  36175  cvmlift3lem4  36177  cvmlift3  36183  brofs  36866  brifs  36904  cgr3permute1  36909  brcolinear2  36919  colineardim1  36922  brfs  36940  btwnconn1  36962  brsegle  36969  unblimceq0  37469  unbdqndv2  37473  rdgeqoa  38402  iscringd  39041  oposlem  40348  ishlat1  40518  3dim1lem5  40632  lvoli2  40747  cdlemk42  42107  diclspsn  42360  monotoddzz  44059  jm2.27  44124  mendlmod  44300  fiiuncl  46190  wessf1ornlem  46308  infleinf  46491  fmulcl  46701  fmuldfeqlem1  46702  fmuldfeq  46703  climinf2mpt  46832  climinfmpt  46833  fprodcncf  47018  dvnmptdivc  47056  dvnprodlem2  47065  dvnprodlem3  47066  stoweidlem6  47124  stoweidlem8  47126  stoweidlem26  47144  stoweidlem31  47149  stoweidlem62  47180  fourierdlem41  47266  fourierdlem48  47272  fourierdlem49  47273  sge0iunmpt  47536  ovnsubaddlem1  47688  isgbe  48957  9gbo  48980  11gbo  48981  sbgoldbst  48984  sbgoldbaltlem1  48985  sbgoldbaltlem2  48986  bgoldbtbndlem4  49014  bgoldbtbnd  49015