Theorem 3anbi23d 1441

Description: Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)

Hypotheses

Ref	Expression
3anbi12d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3anbi12d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
3anbi23d	⊢ (𝜑 → ((𝜂 ∧ 𝜓 ∧ 𝜃) ↔ (𝜂 ∧ 𝜒 ∧ 𝜏)))

Proof of Theorem 3anbi23d

Step	Hyp	Ref	Expression
1		biidd 262	. 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂))
2		3anbi12d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3		3anbi12d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	1, 2, 3	3anbi123d 1438	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:  f1dom3el3dif  7244  xpord2lem  8121  xpord3lem  8128  frecseq123  8261  oeeui  8566  sbthfi  9163  pwfseqlem4a  10614  pwfseqlem4  10615  pfxccatin12lem3  14697  prodeq2w  15876  prodeq2ii  15877  prodeq2sdv  15889  divalg  16373  dfgcd2  16516  iscatd2  17642  posi  18278  issubg3  19076  pmtrfrn  19388  psgnunilem2  19425  psgnunilem3  19426  lmhmpropd  20980  lbsacsbs  21066  frlmphl  21690  neiptoptop  23018  neiptopnei  23019  cnhaus  23241  nrmsep  23244  dishaus  23269  ordthauslem  23270  nconnsubb  23310  pthaus  23525  txhaus  23534  xkohaus  23540  regr1lem  23626  isust  24091  ustuqtop4  24132  methaus  24408  metnrmlem3  24750  iscau4  25179  pmltpclem1  25349  dvfsumlem2  25933  dvfsumlem2OLD  25934  aannenlem1  26236  aannenlem2  26237  brsslt  27697  istrkgcb  28383  hlbtwn  28538  iscgra  28736  dfcgra2  28757  f1otrge  28799  axlowdim  28888  axeuclidlem  28889  eengtrkg  28913  clwwlk  29912  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  numclwwlk5  30317  ex-opab  30361  l2p  30408  vciOLD  30490  isvclem  30506  isnvlem  30539  dipass  30774  adj1  31862  adjeq  31864  cnlnssadj  32009  br8d  32538  dvdsruasso2  33357  dfufd2lem  33520  constrsuc  33728  constrconj  33735  constrllcllem  33742  constrcbvlem  33745  carsgmon  34305  carsgsigalem  34306  carsgclctunlem2  34310  carsgclctun  34312  bnj1154  34989  br8  35743  br6  35744  br4  35745  fvtransport  36020  brcgr3  36034  brfs  36067  fscgr  36068  btwnconn1lem11  36085  brsegle  36096  fvray  36129  linedegen  36131  fvline  36132  cbvproddavw  36268  bj-isclm  37279  poimirlem28  37642  poimirlem32  37646  heiborlem2  37806  hlsuprexch  39375  3dim1lem5  39460  lplni2  39531  2llnjN  39561  lvoli2  39575  2lplnj  39614  cdleme18d  40289  cdlemg1cex  40582  ismrc  42689  monotoddzzfi  42931  oddcomabszz  42933  zindbi  42935  rmydioph  43003  nnoeomeqom  43301  rp-brsslt  43412  fsumiunss  45573  sumnnodd  45628  stoweidlem31  46029  stoweidlem34  46032  stoweidlem43  46041  stoweidlem48  46046  fourierdlem42  46147  sge0iunmptlemre  46413  sge0iunmpt  46416  vonioo  46680  vonicc  46683  fundcmpsurinjpreimafv  47409  upgrimpths  47909  cycl3grtri  47946  grimgrtri  47948  usgrgrtrirex  47949  grlimgrtri  47995  sepfsepc  48916  iscnrm3rlem8  48935  iscnrm3llem2  48938