Theorem 3anbi23d 1442

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 1439	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:  f1dom3el3dif  7218  xpord2lem  8086  xpord3lem  8093  frecseq123  8226  oeeui  8532  sbthfi  9127  pwfseqlem4a  10578  pwfseqlem4  10579  pfxccatin12lem3  14688  prodeq2w  15869  prodeq2ii  15870  prodeq2sdv  15882  divalg  16366  dfgcd2  16509  iscatd2  17641  posi  18277  issubg3  19114  pmtrfrn  19427  psgnunilem2  19464  psgnunilem3  19465  lmhmpropd  21063  lbsacsbs  21149  frlmphl  21774  neiptoptop  23109  neiptopnei  23110  cnhaus  23332  nrmsep  23335  dishaus  23360  ordthauslem  23361  nconnsubb  23401  pthaus  23616  txhaus  23625  xkohaus  23631  regr1lem  23717  isust  24182  ustuqtop4  24222  methaus  24498  metnrmlem3  24840  iscau4  25259  pmltpclem1  25428  dvfsumlem2  26007  aannenlem1  26308  aannenlem2  26309  brslts  27771  bdayfinbndlem1  28476  istrkgcb  28541  hlbtwn  28696  iscgra  28894  dfcgra2  28915  f1otrge  28957  axlowdim  29047  axeuclidlem  29048  eengtrkg  29072  clwwlk  30071  upgr3v3e3cycl  30268  upgr4cycl4dv4e  30273  numclwwlk5  30476  ex-opab  30520  l2p  30568  vciOLD  30650  isvclem  30666  isnvlem  30699  dipass  30934  adj1  32022  adjeq  32024  cnlnssadj  32169  br8d  32699  dvdsruasso2  33464  dfufd2lem  33627  constrsuc  33901  constrconj  33908  constrllcllem  33915  constrcbvlem  33918  carsgmon  34477  carsgsigalem  34478  carsgclctunlem2  34482  carsgclctun  34484  bnj1154  35160  br8  35957  br6  35958  br4  35959  fvtransport  36233  brcgr3  36247  brfs  36280  fscgr  36281  btwnconn1lem11  36298  brsegle  36309  fvray  36342  linedegen  36344  fvline  36345  cbvproddavw  36481  bj-isclm  37624  poimirlem28  37986  poimirlem32  37990  heiborlem2  38150  hlsuprexch  39844  3dim1lem5  39929  lplni2  40000  2llnjN  40030  lvoli2  40044  2lplnj  40083  cdleme18d  40758  cdlemg1cex  41051  ismrc  43150  monotoddzzfi  43391  oddcomabszz  43393  zindbi  43395  rmydioph  43463  nnoeomeqom  43761  rp-brsslt  43871  fsumiunss  46026  sumnnodd  46081  stoweidlem31  46480  stoweidlem34  46483  stoweidlem43  46492  stoweidlem48  46497  fourierdlem42  46598  sge0iunmptlemre  46864  sge0iunmpt  46867  vonioo  47131  vonicc  47134  fundcmpsurinjpreimafv  47883  upgrimpths  48400  cycl3grtri  48438  grimgrtri  48440  usgrgrtrirex  48441  grlimgrtri  48494  sepfsepc  49418  iscnrm3rlem8  49437  iscnrm3llem2  49440