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  3503  ceqsex4v  3504  ceqsex8v  3506  vtocl3gafOLD  3548  vtocl3gaOLD  3550  mob  3688  offval22  8067  smogt  8336  ttrcleq  9662  cfsmolem  10223  fseq1m1p1  13560  pfxsuff1eqwrdeq  14664  2swrd2eqwrdeq  14919  wrdl3s3  14928  prodmo  15902  fprod  15907  divalg  16373  funcres2b  17859  posi  18278  mhmlem  18994  isdrngrd  20675  isdrngrdOLD  20677  lmodlema  20771  connsub  23308  lmmbr3  25160  lmmcvg  25161  dvmptfsum  25879  nosupprefixmo  27612  noinfprefixmo  27613  nosupcbv  27614  nosupno  27615  nosupfv  27618  noinfcbv  27629  noinfno  27630  noinffv  27633  axtg5seg  28392  axtgupdim2  28398  axtgeucl  28399  ishlg  28529  hlcomb  28530  brbtwn  28826  axlowdim  28888  axeuclidlem  28889  usgr2wlkspth  29689  usgr2pth0  29695  wwlksnwwlksnon  29845  umgrwwlks2on  29887  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  nvi  30543  isslmd  33155  slmdlema  33156  opprlidlabs  33456  constrcccllem  33744  constrcbvlem  33745  inelsros  34168  diffiunisros  34169  hgt749d  34640  tgoldbachgt  34654  axtgupdim2ALTV  34659  afsval  34662  brafs  34663  bnj981  34940  bnj1326  35016  cvmlift3lem2  35307  cvmlift3lem4  35309  cvmlift3  35315  brofs  35993  brifs  36031  cgr3permute1  36036  brcolinear2  36046  colineardim1  36049  brfs  36067  btwnconn1  36089  brsegle  36096  unblimceq0  36495  unbdqndv2  36499  rdgeqoa  37358  iscringd  37992  oposlem  39175  ishlat1  39345  3dim1lem5  39460  lvoli2  39575  cdlemk42  40935  diclspsn  41188  monotoddzz  42932  jm2.27  42997  mendlmod  43178  fiiuncl  45059  wessf1ornlem  45179  infleinf  45368  fmulcl  45579  fmuldfeqlem1  45580  fmuldfeq  45581  climinf2mpt  45712  climinfmpt  45713  fprodcncf  45898  dvnmptdivc  45936  dvnprodlem2  45945  dvnprodlem3  45946  stoweidlem6  46004  stoweidlem8  46006  stoweidlem26  46024  stoweidlem31  46029  stoweidlem62  46060  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  sge0iunmpt  46416  ovnsubaddlem1  46568  isgbe  47752  9gbo  47775  11gbo  47776  sbgoldbst  47779  sbgoldbaltlem1  47780  sbgoldbaltlem2  47781  bgoldbtbndlem4  47809  bgoldbtbnd  47810