Theorem 3anbi3d 1468

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  ceqsex3v  3515  ceqsex4v  3516  ceqsex8v  3518  mob  3689  offval22  8082  smogt  8353  ttrcleq  9677  cfsmolem  10253  fseq1m1p1  13626  pfxsuff1eqwrdeq  14735  2swrd2eqwrdeq  14989  wrdl3s3  14998  prodmo  15989  fprod  15994  divalg  16460  funcres2b  17953  posi  18372  mhmlem  19127  isdrngrd  20847  isdrngrdOLD  20849  lmodlema  20963  connsub  23546  lmmbr3  25387  lmmcvg  25388  dvmptfsum  26102  nosupprefixmo  27829  noinfprefixmo  27830  nosupcbv  27831  nosupno  27832  nosupfv  27835  noinfcbv  27846  noinfno  27847  noinffv  27850  bdayfinbndlem2  28626  axtg5seg  28699  axtgupdim2  28705  axtgeucl  28706  ishlg  28836  hlcomb  28837  brbtwn  29189  axlowdim  29251  axeuclidlem  29252  usgr2wlkspth  30048  usgr2pth0  30054  wwlksnwwlksnon  30204  usgrwwlks2on  30247  umgrwwlks2on  30248  upgr3v3e3cycl  30471  upgr4cycl4dv4e  30476  nvi  30906  isslmd  33462  slmdlema  33463  opprlidlabs  33711  constrcccllem  34088  constrcbvlem  34089  inelsros  34512  diffiunisros  34513  hgt749d  34980  tgoldbachgt  34994  axtgupdim2ALTV  34999  afsval  35005  brafs  35006  bnj981  35282  bnj1326  35358  cvmlift3lem2  35710  cvmlift3lem4  35712  cvmlift3  35718  brofs  36395  brifs  36433  cgr3permute1  36438  brcolinear2  36448  colineardim1  36451  brfs  36469  btwnconn1  36491  brsegle  36498  unblimceq0  36984  unbdqndv2  36988  rdgeqoa  37903  iscringd  38536  oposlem  39845  ishlat1  40015  3dim1lem5  40129  lvoli2  40244  cdlemk42  41604  diclspsn  41857  monotoddzz  43561  jm2.27  43626  mendlmod  43807  fiiuncl  45676  wessf1ornlem  45794  infleinf  45978  fmulcl  46188  fmuldfeqlem1  46189  fmuldfeq  46190  climinf2mpt  46319  climinfmpt  46320  fprodcncf  46505  dvnmptdivc  46543  dvnprodlem2  46552  dvnprodlem3  46553  stoweidlem6  46611  stoweidlem8  46613  stoweidlem26  46631  stoweidlem31  46636  stoweidlem62  46667  fourierdlem41  46753  fourierdlem48  46759  fourierdlem49  46760  sge0iunmpt  47023  ovnsubaddlem1  47175  isgbe  48404  9gbo  48427  11gbo  48428  sbgoldbst  48431  sbgoldbaltlem1  48432  sbgoldbaltlem2  48433  bgoldbtbndlem4  48461  bgoldbtbnd  48462