Theorem 3anbi23d 1466

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104

This theorem is used by:  f1dom3el3dif  7267  xpord2lem  8136  xpord3lem  8143  frecseq123  8277  oeeui  8586  sbthfi  9181  pwfseqlem4a  10652  pwfseqlem4  10653  pfxccatin12lem3  14776  prodeq2w  15971  prodeq2ii  15972  prodeq2sdv  15984  divalg  16467  dfgcd2  16610  iscatd2  17743  posi  18379  issubg3  19217  pmtrfrn  19534  psgnunilem2  19571  psgnunilem3  19572  lmhmpropd  21205  lbsacsbs  21291  frlmphl  21942  neiptoptop  23299  neiptopnei  23300  cnhaus  23522  nrmsep  23525  dishaus  23550  ordthauslem  23551  nconnsubb  23591  pthaus  23806  txhaus  23815  xkohaus  23821  regr1lem  23907  isust  24372  ustuqtop4  24412  methaus  24688  metnrmlem3  25030  iscau4  25449  pmltpclem1  25618  dvfsumlem2  26197  aannenlem1  26502  aannenlem2  26503  brslts  27966  bdayfinbndlem1  28671  istrkgcb  28736  hlbtwn  28894  iscgra  29131  dfcgra2  29152  f1otrge  29232  axlowdim  29322  axeuclidlem  29323  eengtrkg  29347  clwwlk  30345  upgr3v3e3cycl  30542  upgr4cycl4dv4e  30547  numclwwlk5  30750  ex-opab  30794  l2p  30842  vciOLD  30924  isvclem  30940  isnvlem  30973  dipass  31208  adj1  32296  adjeq  32298  cnlnssadj  32443  br8d  32964  dvdsruasso2  33708  dfufd2lem  33848  constrsuc  34137  constrconj  34144  constrllcllem  34151  constrcbvlem  34154  carsgmon  34713  carsgsigalem  34714  carsgclctunlem2  34718  carsgclctun  34720  bnj1154  35396  br8  36256  br6  36257  br4  36258  fvtransport  36532  brcgr3  36546  brfs  36579  fscgr  36580  btwnconn1lem11  36597  brsegle  36608  fvray  36641  linedegen  36643  fvline  36644  cbvproddavw  36820  bj-isclm  37963  poimirlem28  38327  poimirlem32  38331  heiborlem2  38491  hlsuprexch  40183  3dim1lem5  40268  lplni2  40339  2llnjN  40369  lvoli2  40383  2lplnj  40422  cdleme18d  41097  cdlemg1cex  41390  ismrc  43460  monotoddzzfi  43697  oddcomabszz  43699  zindbi  43701  rmydioph  43769  nnoeomeqom  44067  rp-brsslt  44177  fsumiunss  46319  sumnnodd  46374  stoweidlem31  46773  stoweidlem34  46776  stoweidlem43  46785  stoweidlem48  46790  fourierdlem42  46891  sge0iunmptlemre  47157  sge0iunmpt  47160  vonioo  47424  vonicc  47427  fundcmpsurinjpreimafv  48185  upgrimpths  48702  cycl3grtri  48740  grimgrtri  48742  usgrgrtrirex  48743  grlimgrtri  48796  sepfsepc  49734  iscnrm3rlem8  49753  iscnrm3llem2  49756