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  3492  ceqsex4v  3493  ceqsex8v  3495  vtocl3gafOLD  3537  vtocl3gaOLD  3539  mob  3677  offval22  8021  smogt  8290  ttrcleq  9605  cfsmolem  10164  fseq1m1p1  13502  pfxsuff1eqwrdeq  14605  2swrd2eqwrdeq  14860  wrdl3s3  14869  prodmo  15843  fprod  15848  divalg  16314  funcres2b  17804  posi  18223  mhmlem  18941  isdrngrd  20651  isdrngrdOLD  20653  lmodlema  20768  connsub  23306  lmmbr3  25158  lmmcvg  25159  dvmptfsum  25877  nosupprefixmo  27610  noinfprefixmo  27611  nosupcbv  27612  nosupno  27613  nosupfv  27616  noinfcbv  27627  noinfno  27628  noinffv  27631  axtg5seg  28410  axtgupdim2  28416  axtgeucl  28417  ishlg  28547  hlcomb  28548  brbtwn  28844  axlowdim  28906  axeuclidlem  28907  usgr2wlkspth  29704  usgr2pth0  29710  wwlksnwwlksnon  29860  umgrwwlks2on  29902  upgr3v3e3cycl  30124  upgr4cycl4dv4e  30129  nvi  30558  isslmd  33144  slmdlema  33145  opprlidlabs  33422  constrcccllem  33721  constrcbvlem  33722  inelsros  34145  diffiunisros  34146  hgt749d  34617  tgoldbachgt  34631  axtgupdim2ALTV  34636  afsval  34639  brafs  34640  bnj981  34917  bnj1326  34993  cvmlift3lem2  35293  cvmlift3lem4  35295  cvmlift3  35301  brofs  35979  brifs  36017  cgr3permute1  36022  brcolinear2  36032  colineardim1  36035  brfs  36053  btwnconn1  36075  brsegle  36082  unblimceq0  36481  unbdqndv2  36485  rdgeqoa  37344  iscringd  37978  oposlem  39161  ishlat1  39331  3dim1lem5  39445  lvoli2  39560  cdlemk42  40920  diclspsn  41173  monotoddzz  42916  jm2.27  42981  mendlmod  43162  fiiuncl  45043  wessf1ornlem  45163  infleinf  45351  fmulcl  45562  fmuldfeqlem1  45563  fmuldfeq  45564  climinf2mpt  45695  climinfmpt  45696  fprodcncf  45881  dvnmptdivc  45919  dvnprodlem2  45928  dvnprodlem3  45929  stoweidlem6  45987  stoweidlem8  45989  stoweidlem26  46007  stoweidlem31  46012  stoweidlem62  46043  fourierdlem41  46129  fourierdlem48  46135  fourierdlem49  46136  sge0iunmpt  46399  ovnsubaddlem1  46551  isgbe  47735  9gbo  47758  11gbo  47759  sbgoldbst  47762  sbgoldbaltlem1  47763  sbgoldbaltlem2  47764  bgoldbtbndlem4  47792  bgoldbtbnd  47793