Theorem 3anbi23d 1465

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 265	. 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂))
2		3anbi12d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3		3anbi12d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	1, 2, 3	3anbi123d 1462	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:  f1dom3el3dif  7268  xpord2lem  8138  xpord3lem  8145  frecseq123  8279  oeeui  8588  sbthfi  9183  pwfseqlem4a  10646  pwfseqlem4  10647  pfxccatin12lem3  14769  prodeq2w  15964  prodeq2ii  15965  prodeq2sdv  15977  divalg  16461  dfgcd2  16604  iscatd2  17737  posi  18373  issubg3  19211  pmtrfrn  19528  psgnunilem2  19565  psgnunilem3  19566  lmhmpropd  21172  lbsacsbs  21258  frlmphl  21900  neiptoptop  23257  neiptopnei  23258  cnhaus  23480  nrmsep  23483  dishaus  23508  ordthauslem  23509  nconnsubb  23549  pthaus  23764  txhaus  23773  xkohaus  23779  regr1lem  23865  isust  24330  ustuqtop4  24370  methaus  24646  metnrmlem3  24988  iscau4  25407  pmltpclem1  25576  dvfsumlem2  26155  aannenlem1  26458  aannenlem2  26459  brslts  27921  bdayfinbndlem1  28626  istrkgcb  28691  hlbtwn  28846  iscgra  29077  dfcgra2  29098  f1otrge  29162  axlowdim  29252  axeuclidlem  29253  eengtrkg  29277  clwwlk  30275  upgr3v3e3cycl  30472  upgr4cycl4dv4e  30477  numclwwlk5  30680  ex-opab  30724  l2p  30772  vciOLD  30854  isvclem  30870  isnvlem  30903  dipass  31138  adj1  32226  adjeq  32228  cnlnssadj  32373  br8d  32894  dvdsruasso2  33643  dfufd2lem  33784  constrsuc  34073  constrconj  34080  constrllcllem  34087  constrcbvlem  34090  carsgmon  34649  carsgsigalem  34650  carsgclctunlem2  34654  carsgclctun  34656  bnj1154  35332  br8  36181  br6  36182  br4  36183  fvtransport  36457  brcgr3  36471  brfs  36504  fscgr  36505  btwnconn1lem11  36522  brsegle  36533  fvray  36566  linedegen  36568  fvline  36569  cbvproddavw  36715  bj-isclm  37857  poimirlem28  38221  poimirlem32  38225  heiborlem2  38385  hlsuprexch  40079  3dim1lem5  40164  lplni2  40235  2llnjN  40265  lvoli2  40279  2lplnj  40318  cdleme18d  40993  cdlemg1cex  41286  ismrc  43358  monotoddzzfi  43595  oddcomabszz  43597  zindbi  43599  rmydioph  43667  nnoeomeqom  43965  rp-brsslt  44075  fsumiunss  46217  sumnnodd  46272  stoweidlem31  46671  stoweidlem34  46674  stoweidlem43  46683  stoweidlem48  46688  fourierdlem42  46789  sge0iunmptlemre  47055  sge0iunmpt  47058  vonioo  47322  vonicc  47325  fundcmpsurinjpreimafv  48080  upgrimpths  48597  cycl3grtri  48635  grimgrtri  48637  usgrgrtrirex  48638  grlimgrtri  48691  sepfsepc  49625  iscnrm3rlem8  49644  iscnrm3llem2  49647