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  7213  xpord2lem  8082  xpord3lem  8089  frecseq123  8222  oeeui  8528  sbthfi  9121  pwfseqlem4a  10570  pwfseqlem4  10571  pfxccatin12lem3  14653  prodeq2w  15831  prodeq2ii  15832  prodeq2sdv  15844  divalg  16328  dfgcd2  16471  iscatd2  17602  posi  18238  issubg3  19072  pmtrfrn  19385  psgnunilem2  19422  psgnunilem3  19423  lmhmpropd  21023  lbsacsbs  21109  frlmphl  21734  neiptoptop  23073  neiptopnei  23074  cnhaus  23296  nrmsep  23299  dishaus  23324  ordthauslem  23325  nconnsubb  23365  pthaus  23580  txhaus  23589  xkohaus  23595  regr1lem  23681  isust  24146  ustuqtop4  24186  methaus  24462  metnrmlem3  24804  iscau4  25233  pmltpclem1  25403  dvfsumlem2  25987  dvfsumlem2OLD  25988  aannenlem1  26290  aannenlem2  26291  brsslt  27752  istrkgcb  28477  hlbtwn  28632  iscgra  28830  dfcgra2  28851  f1otrge  28893  axlowdim  28983  axeuclidlem  28984  eengtrkg  29008  clwwlk  30007  upgr3v3e3cycl  30204  upgr4cycl4dv4e  30209  numclwwlk5  30412  ex-opab  30456  l2p  30503  vciOLD  30585  isvclem  30601  isnvlem  30634  dipass  30869  adj1  31957  adjeq  31959  cnlnssadj  32104  br8d  32635  dvdsruasso2  33416  dfufd2lem  33579  constrsuc  33844  constrconj  33851  constrllcllem  33858  constrcbvlem  33861  carsgmon  34420  carsgsigalem  34421  carsgclctunlem2  34425  carsgclctun  34427  bnj1154  35104  br8  35899  br6  35900  br4  35901  fvtransport  36175  brcgr3  36189  brfs  36222  fscgr  36223  btwnconn1lem11  36240  brsegle  36251  fvray  36284  linedegen  36286  fvline  36287  cbvproddavw  36423  bj-isclm  37435  poimirlem28  37788  poimirlem32  37792  heiborlem2  37952  hlsuprexch  39580  3dim1lem5  39665  lplni2  39736  2llnjN  39766  lvoli2  39780  2lplnj  39819  cdleme18d  40494  cdlemg1cex  40787  ismrc  42885  monotoddzzfi  43126  oddcomabszz  43128  zindbi  43130  rmydioph  43198  nnoeomeqom  43496  rp-brsslt  43606  fsumiunss  45763  sumnnodd  45818  stoweidlem31  46217  stoweidlem34  46220  stoweidlem43  46229  stoweidlem48  46234  fourierdlem42  46335  sge0iunmptlemre  46601  sge0iunmpt  46604  vonioo  46868  vonicc  46871  fundcmpsurinjpreimafv  47596  upgrimpths  48097  cycl3grtri  48135  grimgrtri  48137  usgrgrtrirex  48138  grlimgrtri  48191  sepfsepc  49115  iscnrm3rlem8  49134  iscnrm3llem2  49137