Theorem 3anbi3d 1444

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  ceqsex3v  3495  ceqsex4v  3496  ceqsex8v  3498  vtocl3gafOLD  3537  vtocl3gaOLD  3539  mob  3675  offval22  8030  smogt  8299  ttrcleq  9618  cfsmolem  10180  fseq1m1p1  13515  pfxsuff1eqwrdeq  14622  2swrd2eqwrdeq  14876  wrdl3s3  14885  prodmo  15859  fprod  15864  divalg  16330  funcres2b  17821  posi  18240  mhmlem  18992  isdrngrd  20699  isdrngrdOLD  20701  lmodlema  20816  connsub  23365  lmmbr3  25216  lmmcvg  25217  dvmptfsum  25935  nosupprefixmo  27668  noinfprefixmo  27669  nosupcbv  27670  nosupno  27671  nosupfv  27674  noinfcbv  27685  noinfno  27686  noinffv  27689  bdayfinbndlem2  28464  axtg5seg  28537  axtgupdim2  28543  axtgeucl  28544  ishlg  28674  hlcomb  28675  brbtwn  28972  axlowdim  29034  axeuclidlem  29035  usgr2wlkspth  29832  usgr2pth0  29838  wwlksnwwlksnon  29988  usgrwwlks2on  30031  umgrwwlks2on  30032  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  nvi  30689  isslmd  33284  slmdlema  33285  opprlidlabs  33566  constrcccllem  33911  constrcbvlem  33912  inelsros  34335  diffiunisros  34336  hgt749d  34806  tgoldbachgt  34820  axtgupdim2ALTV  34825  afsval  34828  brafs  34829  bnj981  35106  bnj1326  35182  cvmlift3lem2  35514  cvmlift3lem4  35516  cvmlift3  35522  brofs  36199  brifs  36237  cgr3permute1  36242  brcolinear2  36252  colineardim1  36255  brfs  36273  btwnconn1  36295  brsegle  36302  unblimceq0  36707  unbdqndv2  36711  rdgeqoa  37575  iscringd  38199  oposlem  39442  ishlat1  39612  3dim1lem5  39726  lvoli2  39841  cdlemk42  41201  diclspsn  41454  monotoddzz  43185  jm2.27  43250  mendlmod  43431  fiiuncl  45310  wessf1ornlem  45429  infleinf  45616  fmulcl  45827  fmuldfeqlem1  45828  fmuldfeq  45829  climinf2mpt  45958  climinfmpt  45959  fprodcncf  46144  dvnmptdivc  46182  dvnprodlem2  46191  dvnprodlem3  46192  stoweidlem6  46250  stoweidlem8  46252  stoweidlem26  46270  stoweidlem31  46275  stoweidlem62  46306  fourierdlem41  46392  fourierdlem48  46398  fourierdlem49  46399  sge0iunmpt  46662  ovnsubaddlem1  46814  isgbe  47997  9gbo  48020  11gbo  48021  sbgoldbst  48024  sbgoldbaltlem1  48025  sbgoldbaltlem2  48026  bgoldbtbndlem4  48054  bgoldbtbnd  48055