Theorem 3anbi3d 1440

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  ceqsex3v  3474  ceqsex4v  3475  ceqsex8v  3477  vtocl3gaf  3506  vtocl3ga  3507  mob  3647  dfopif  4797  offval22  7899  smogt  8169  cfsmolem  9957  fseq1m1p1  13260  pfxsuff1eqwrdeq  14340  2swrd2eqwrdeq  14594  wrdl3s3  14605  prodmo  15574  fprod  15579  divalg  16040  funcres2b  17528  posi  17950  mhmlem  18610  isdrngrd  19932  lmodlema  20043  connsub  22480  lmmbr3  24329  lmmcvg  24330  dvmptfsum  25044  axtg5seg  26730  axtgupdim2  26736  axtgeucl  26737  ishlg  26867  hlcomb  26868  brbtwn  27170  axlowdim  27232  axeuclidlem  27233  usgr2wlkspth  28028  usgr2pth0  28034  wwlksnwwlksnon  28181  umgrwwlks2on  28223  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  nvi  28877  isslmd  31357  slmdlema  31358  inelsros  32046  diffiunisros  32047  hgt749d  32529  tgoldbachgt  32543  axtgupdim2ALTV  32548  afsval  32551  brafs  32552  bnj981  32830  bnj1326  32906  cvmlift3lem2  33182  cvmlift3lem4  33184  cvmlift3  33190  ttrcleq  33695  nosupprefixmo  33830  noinfprefixmo  33831  nosupcbv  33832  nosupno  33833  nosupfv  33836  noinfcbv  33847  noinfno  33848  noinffv  33851  brofs  34234  brifs  34272  cgr3permute1  34277  brcolinear2  34287  colineardim1  34290  brfs  34308  btwnconn1  34330  brsegle  34337  unblimceq0  34614  unbdqndv2  34618  rdgeqoa  35468  iscringd  36083  oposlem  37123  ishlat1  37293  3dim1lem5  37407  lvoli2  37522  cdlemk42  38882  diclspsn  39135  monotoddzz  40681  jm2.27  40746  mendlmod  40934  fiiuncl  42502  wessf1ornlem  42611  infleinf  42801  fmulcl  43012  fmuldfeqlem1  43013  fmuldfeq  43014  climinf2mpt  43145  climinfmpt  43146  fprodcncf  43331  dvnmptdivc  43369  dvnprodlem2  43378  dvnprodlem3  43379  stoweidlem6  43437  stoweidlem8  43439  stoweidlem26  43457  stoweidlem31  43462  stoweidlem62  43493  fourierdlem41  43579  fourierdlem48  43585  fourierdlem49  43586  sge0iunmpt  43846  ovnsubaddlem1  43998  isgbe  45091  9gbo  45114  11gbo  45115  sbgoldbst  45118  sbgoldbaltlem1  45119  sbgoldbaltlem2  45120  bgoldbtbndlem4  45148  bgoldbtbnd  45149