Theorem 3anbi23d 1419

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ w3a 1069

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 199  df-an 388  df-3an 1071

This theorem is referenced by:  f1dom3el3dif  6850  wrecseq123  7749  oeeui  8027  fpwwe2lem5  9852  pwfseqlem4a  9879  pwfseqlem4  9880  swrdccatin12lem3  13931  prodeq2w  15124  prodeq2ii  15125  divalg  15612  dfgcd2  15748  iscatd2  16822  posi  17430  issubg3  18093  pmtrfrn  18359  psgnunilem2  18397  psgnunilem3  18398  lmhmpropd  19579  lbsacsbs  19662  frlmphl  20642  neiptoptop  21458  neiptopnei  21459  cnhaus  21681  nrmsep  21684  dishaus  21709  ordthauslem  21710  nconnsubb  21750  pthaus  21965  txhaus  21974  xkohaus  21980  regr1lem  22066  isust  22530  ustuqtop4  22571  methaus  22848  metnrmlem3  23187  iscau4  23600  pmltpclem1  23767  dvfsumlem2  24342  aannenlem1  24635  aannenlem2  24636  istrkgcb  25959  hlbtwn  26114  iscgra  26312  dfcgra2  26333  f1otrge  26376  axlowdim  26465  axeuclidlem  26466  eengtrkg  26490  clwwlk  27504  upgr3v3e3cycl  27724  upgr4cycl4dv4e  27729  numclwwlk5  27960  ex-opab  28004  l2p  28048  vciOLD  28130  isvclem  28146  isnvlem  28179  dipass  28414  adj1  29506  adjeq  29508  cnlnssadj  29653  br8d  30142  carsgmon  31249  carsgsigalem  31250  carsgclctunlem2  31254  carsgclctun  31256  bnj1154  31948  br8  32549  br6  32550  br4  32551  frecseq123  32677  brsslt  32812  fvtransport  33051  brcgr3  33065  brfs  33098  fscgr  33099  btwnconn1lem11  33116  brsegle  33127  fvray  33160  linedegen  33162  fvline  33163  poimirlem28  34398  poimirlem32  34402  heiborlem2  34569  hlsuprexch  35999  3dim1lem5  36084  lplni2  36155  2llnjN  36185  lvoli2  36199  2lplnj  36238  cdleme18d  36913  cdlemg1cex  37206  ismrc  38731  monotoddzzfi  38973  oddcomabszz  38975  zindbi  38977  rmydioph  39045  fsumiunss  41321  sumnnodd  41376  stoweidlem31  41781  stoweidlem34  41784  stoweidlem43  41793  stoweidlem48  41798  fourierdlem42  41899  sge0iunmptlemre  42162  sge0iunmpt  42165  vonioo  42429  vonicc  42432