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  3503  ceqsex4v  3504  ceqsex8v  3506  mob  3675  offval22  8097  smogt  8368  ttrcleq  9703  cfsmolem  10341  fseq1m1p1  13726  pfxsuff1eqwrdeq  14841  2swrd2eqwrdeq  15099  wrdl3s3  15108  prodmo  16096  fprod  16101  divalg  16566  funcres2b  18065  posi  18484  mhmlem  19265  isdrngrd  21016  isdrngrdOLD  21018  lmodlema  21133  connsub  23732  lmmbr3  25574  lmmcvg  25575  dvmptfsum  26288  nosupprefixmo  28050  noinfprefixmo  28051  nosupcbv  28052  nosupno  28053  nosupfv  28056  noinfcbv  28067  noinfno  28068  noinffv  28071  bdayfinbndlem2  28847  axtg5seg  28920  axtgupdim2  28926  axtgeucl  28927  ishlg2  29058  ishlg  29061  hlcomb  29062  brbtwn  29470  axlowdim  29532  axeuclidlem  29533  usgr2wlkspth  30338  usgr2pth0  30344  wwlksnwwlksnon  30497  usgrwwlks2on  30540  umgrwwlks2on  30541  upgr3v3e3cycl  30774  upgr4cycl4dv4e  30779  nvi  31209  isslmd  33756  slmdlema  33757  opprlidlabs  34002  constrcccllem  34379  constrcbvlem  34380  inelsros  34804  diffiunisros  34805  hgt749d  35271  tgoldbachgt  35285  axtgupdim2ALTV  35290  afsval  35296  brafs  35297  bnj981  35573  bnj1326  35649  cvmlift3lem2  36064  cvmlift3lem4  36066  cvmlift3  36072  brofs  36750  brifs  36788  cgr3permute1  36793  brcolinear2  36803  colineardim1  36806  brfs  36824  btwnconn1  36846  brsegle  36853  unblimceq0  37353  unbdqndv2  37357  rdgeqoa  38273  iscringd  38912  oposlem  40219  ishlat1  40389  3dim1lem5  40503  lvoli2  40618  cdlemk42  41978  diclspsn  42231  monotoddzz  43929  jm2.27  43994  mendlmod  44175  fiiuncl  46051  wessf1ornlem  46169  infleinf  46352  fmulcl  46562  fmuldfeqlem1  46563  fmuldfeq  46564  climinf2mpt  46693  climinfmpt  46694  fprodcncf  46879  dvnmptdivc  46917  dvnprodlem2  46926  dvnprodlem3  46927  stoweidlem6  46985  stoweidlem8  46987  stoweidlem26  47005  stoweidlem31  47010  stoweidlem62  47041  fourierdlem41  47127  fourierdlem48  47133  fourierdlem49  47134  sge0iunmpt  47397  ovnsubaddlem1  47549  isgbe  48818  9gbo  48841  11gbo  48842  sbgoldbst  48845  sbgoldbaltlem1  48846  sbgoldbaltlem2  48847  bgoldbtbndlem4  48875  bgoldbtbnd  48876