Theorem 3anbi3d 1471

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 1467	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  3506  ceqsex4v  3507  ceqsex8v  3509  mob  3678  offval22  8134  smogt  8413  ttrcleq  9747  cfsmolem  10387  fseq1m1p1  13773  pfxsuff1eqwrdeq  14890  2swrd2eqwrdeq  15149  wrdl3s3  15158  prodmo  16147  fprod  16152  divalg  16617  funcres2b  18122  posi  18541  mhmlem  19322  isdrngrd  21074  isdrngrdOLD  21076  lmodlema  21191  connsub  23794  lmmbr3  25636  lmmcvg  25637  dvmptfsum  26350  nosupprefixmo  28114  noinfprefixmo  28115  nosupcbv  28116  nosupno  28117  nosupfv  28120  noinfcbv  28131  noinfno  28132  noinffv  28135  bdayfinbndlem2  28911  axtg5seg  28984  axtgupdim2  28990  axtgeucl  28991  ishlg2  29122  ishlg  29125  hlcomb  29126  brbtwn  29534  axlowdim  29596  axeuclidlem  29597  usgr2wlkspth  30402  usgr2pth0  30408  wwlksnwwlksnon  30561  usgrwwlks2on  30604  umgrwwlks2on  30605  upgr3v3e3cycl  30838  upgr4cycl4dv4e  30843  nvi  31273  isslmd  33862  slmdlema  33863  opprlidlabs  34113  constrcccllem  34497  constrcbvlem  34498  inelsros  34922  diffiunisros  34923  hgt749d  35389  tgoldbachgt  35403  axtgupdim2ALTV  35408  afsval  35414  brafs  35415  bnj981  35691  bnj1326  35767  cvmlift3lem2  36293  cvmlift3lem4  36295  cvmlift3  36301  brofs  36985  brifs  37023  cgr3permute1  37028  brcolinear2  37038  colineardim1  37041  brfs  37059  btwnconn1  37081  brsegle  37088  unblimceq0  37588  unbdqndv2  37592  rdgeqoa  38561  iscringd  39198  oposlem  40505  ishlat1  40675  3dim1lem5  40789  lvoli2  40904  cdlemk42  42264  diclspsn  42517  monotoddzz  44216  jm2.27  44281  mendlmod  44452  fiiuncl  46356  wessf1ornlem  46473  infleinf  46656  fmulcl  46866  fmuldfeqlem1  46867  fmuldfeq  46868  climinf2mpt  46997  climinfmpt  46998  fprodcncf  47183  dvnmptdivc  47221  dvnprodlem2  47230  dvnprodlem3  47231  stoweidlem6  47289  stoweidlem8  47291  stoweidlem26  47309  stoweidlem31  47314  stoweidlem62  47345  fourierdlem41  47431  fourierdlem48  47437  fourierdlem49  47438  sge0iunmpt  47701  ovnsubaddlem1  47853  isgbe  49122  9gbo  49145  11gbo  49146  sbgoldbst  49149  sbgoldbaltlem1  49150  sbgoldbaltlem2  49151  bgoldbtbndlem4  49179  bgoldbtbnd  49180