Theorem 3anbi3d 1445

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 1441	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜏 ∧ 𝜓) ↔ (𝜃 ∧ 𝜏 ∧ 𝜒)))

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

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 1089

This theorem is referenced by:  ceqsex3v  3497  ceqsex4v  3498  ceqsex8v  3500  vtocl3gafOLD  3539  vtocl3gaOLD  3541  mob  3677  offval22  8040  smogt  8309  ttrcleq  9630  cfsmolem  10192  fseq1m1p1  13527  pfxsuff1eqwrdeq  14634  2swrd2eqwrdeq  14888  wrdl3s3  14897  prodmo  15871  fprod  15876  divalg  16342  funcres2b  17833  posi  18252  mhmlem  19004  isdrngrd  20711  isdrngrdOLD  20713  lmodlema  20828  connsub  23377  lmmbr3  25228  lmmcvg  25229  dvmptfsum  25947  nosupprefixmo  27680  noinfprefixmo  27681  nosupcbv  27682  nosupno  27683  nosupfv  27686  noinfcbv  27697  noinfno  27698  noinffv  27701  bdayfinbndlem2  28476  axtg5seg  28549  axtgupdim2  28555  axtgeucl  28556  ishlg  28686  hlcomb  28687  brbtwn  28984  axlowdim  29046  axeuclidlem  29047  usgr2wlkspth  29844  usgr2pth0  29850  wwlksnwwlksnon  30000  usgrwwlks2on  30043  umgrwwlks2on  30044  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  nvi  30702  isslmd  33296  slmdlema  33297  opprlidlabs  33578  constrcccllem  33932  constrcbvlem  33933  inelsros  34356  diffiunisros  34357  hgt749d  34827  tgoldbachgt  34841  axtgupdim2ALTV  34846  afsval  34849  brafs  34850  bnj981  35126  bnj1326  35202  cvmlift3lem2  35536  cvmlift3lem4  35538  cvmlift3  35544  brofs  36221  brifs  36259  cgr3permute1  36264  brcolinear2  36274  colineardim1  36277  brfs  36295  btwnconn1  36317  brsegle  36324  unblimceq0  36729  unbdqndv2  36733  rdgeqoa  37625  iscringd  38249  oposlem  39558  ishlat1  39728  3dim1lem5  39842  lvoli2  39957  cdlemk42  41317  diclspsn  41570  monotoddzz  43300  jm2.27  43365  mendlmod  43546  fiiuncl  45425  wessf1ornlem  45544  infleinf  45730  fmulcl  45941  fmuldfeqlem1  45942  fmuldfeq  45943  climinf2mpt  46072  climinfmpt  46073  fprodcncf  46258  dvnmptdivc  46296  dvnprodlem2  46305  dvnprodlem3  46306  stoweidlem6  46364  stoweidlem8  46366  stoweidlem26  46384  stoweidlem31  46389  stoweidlem62  46420  fourierdlem41  46506  fourierdlem48  46512  fourierdlem49  46513  sge0iunmpt  46776  ovnsubaddlem1  46928  isgbe  48111  9gbo  48134  11gbo  48135  sbgoldbst  48138  sbgoldbaltlem1  48139  sbgoldbaltlem2  48140  bgoldbtbndlem4  48168  bgoldbtbnd  48169