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  3509  ceqsex4v  3510  ceqsex8v  3512  mob  3682  offval22  8089  smogt  8360  ttrcleq  9685  cfsmolem  10269  fseq1m1p1  13644  pfxsuff1eqwrdeq  14758  2swrd2eqwrdeq  15014  wrdl3s3  15023  prodmo  16013  fprod  16018  divalg  16483  funcres2b  17976  posi  18395  mhmlem  19172  isdrngrd  20919  isdrngrdOLD  20921  lmodlema  21036  connsub  23628  lmmbr3  25470  lmmcvg  25471  dvmptfsum  26185  nosupprefixmo  27915  noinfprefixmo  27916  nosupcbv  27917  nosupno  27918  nosupfv  27921  noinfcbv  27932  noinfno  27933  noinffv  27936  bdayfinbndlem2  28712  axtg5seg  28785  axtgupdim2  28791  axtgeucl  28792  ishlg2  28922  ishlg  28925  hlcomb  28926  brbtwn  29304  axlowdim  29366  axeuclidlem  29367  usgr2wlkspth  30172  usgr2pth0  30178  wwlksnwwlksnon  30331  usgrwwlks2on  30374  umgrwwlks2on  30375  upgr3v3e3cycl  30602  upgr4cycl4dv4e  30607  nvi  31037  isslmd  33586  slmdlema  33587  opprlidlabs  33831  constrcccllem  34208  constrcbvlem  34209  inelsros  34633  diffiunisros  34634  hgt749d  35101  tgoldbachgt  35115  axtgupdim2ALTV  35120  afsval  35126  brafs  35127  bnj981  35403  bnj1326  35479  cvmlift3lem2  35849  cvmlift3lem4  35851  cvmlift3  35857  brofs  36534  brifs  36572  cgr3permute1  36577  brcolinear2  36587  colineardim1  36590  brfs  36608  btwnconn1  36630  brsegle  36637  unblimceq0  37153  unbdqndv2  37157  rdgeqoa  38073  iscringd  38707  oposlem  40014  ishlat1  40184  3dim1lem5  40298  lvoli2  40413  cdlemk42  41773  diclspsn  42026  monotoddzz  43728  jm2.27  43793  mendlmod  43974  fiiuncl  45843  wessf1ornlem  45961  infleinf  46145  fmulcl  46355  fmuldfeqlem1  46356  fmuldfeq  46357  climinf2mpt  46486  climinfmpt  46487  fprodcncf  46672  dvnmptdivc  46710  dvnprodlem2  46719  dvnprodlem3  46720  stoweidlem6  46778  stoweidlem8  46780  stoweidlem26  46798  stoweidlem31  46803  stoweidlem62  46834  fourierdlem41  46920  fourierdlem48  46926  fourierdlem49  46927  sge0iunmpt  47190  ovnsubaddlem1  47342  isgbe  48574  9gbo  48597  11gbo  48598  sbgoldbst  48601  sbgoldbaltlem1  48602  sbgoldbaltlem2  48603  bgoldbtbndlem4  48631  bgoldbtbnd  48632