Theorem 3anbi23d 1447

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 263	. 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂))
2		3anbi12d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3		3anbi12d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	1, 2, 3	3anbi123d 1444	1 ⊢ (𝜑 → ((𝜂 ∧ 𝜓 ∧ 𝜃) ↔ (𝜂 ∧ 𝜒 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  f1dom3el3dif  7213  xpord2lem  8082  xpord3lem  8089  frecseq123  8222  oeeui  8528  sbthfi  9123  pwfseqlem4a  10575  pwfseqlem4  10576  pfxccatin12lem3  14685  prodeq2w  15866  prodeq2ii  15867  prodeq2sdv  15879  divalg  16363  dfgcd2  16506  iscatd2  17638  posi  18274  issubg3  19111  pmtrfrn  19424  psgnunilem2  19461  psgnunilem3  19462  lmhmpropd  21063  lbsacsbs  21149  frlmphl  21756  neiptoptop  23114  neiptopnei  23115  cnhaus  23337  nrmsep  23340  dishaus  23365  ordthauslem  23366  nconnsubb  23406  pthaus  23621  txhaus  23630  xkohaus  23636  regr1lem  23722  isust  24187  ustuqtop4  24227  methaus  24503  metnrmlem3  24845  iscau4  25264  pmltpclem1  25433  dvfsumlem2  26012  aannenlem1  26312  aannenlem2  26313  brslts  27772  bdayfinbndlem1  28477  istrkgcb  28542  hlbtwn  28697  iscgra  28895  dfcgra2  28916  f1otrge  28958  axlowdim  29048  axeuclidlem  29049  eengtrkg  29073  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  32700  dvdsruasso2  33469  dfufd2lem  33632  constrsuc  33922  constrconj  33929  constrllcllem  33936  constrcbvlem  33939  carsgmon  34498  carsgsigalem  34499  carsgclctunlem2  34503  carsgclctun  34505  bnj1154  35181  br8  35984  br6  35985  br4  35986  fvtransport  36260  brcgr3  36274  brfs  36307  fscgr  36308  btwnconn1lem11  36325  brsegle  36336  fvray  36369  linedegen  36371  fvline  36372  cbvproddavw  36508  bj-isclm  37651  poimirlem28  38015  poimirlem32  38019  heiborlem2  38179  hlsuprexch  39873  3dim1lem5  39958  lplni2  40029  2llnjN  40059  lvoli2  40073  2lplnj  40112  cdleme18d  40787  cdlemg1cex  41080  ismrc  43150  monotoddzzfi  43387  oddcomabszz  43389  zindbi  43391  rmydioph  43459  nnoeomeqom  43757  rp-brsslt  43867  fsumiunss  46020  sumnnodd  46075  stoweidlem31  46474  stoweidlem34  46477  stoweidlem43  46486  stoweidlem48  46491  fourierdlem42  46592  sge0iunmptlemre  46858  sge0iunmpt  46861  vonioo  47125  vonicc  47128  fundcmpsurinjpreimafv  47883  upgrimpths  48400  cycl3grtri  48438  grimgrtri  48440  usgrgrtrirex  48441  grlimgrtri  48494  sepfsepc  49418  iscnrm3rlem8  49437  iscnrm3llem2  49440