Theorem 3anbi23d 1467

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

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

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 402  df-3an 1105

This theorem is used by:  f1dom3el3dif  7273  xpord2lem  8159  xpord3lem  8166  frecseq123  8300  oeeui  8611  sbthfi  9214  pwfseqlem4a  10746  pwfseqlem4  10747  pfxccatin12lem3  14881  prodeq2w  16079  prodeq2ii  16080  prodeq2sdv  16091  divalg  16573  dfgcd2  16719  iscatd2  17855  posi  18491  issubg3  19355  pmtrfrn  19672  psgnunilem2  19709  psgnunilem3  19710  lmhmpropd  21348  lbsacsbs  21434  frlmphl  22087  neiptoptop  23449  neiptopnei  23450  cnhaus  23672  nrmsep  23675  dishaus  23700  ordthauslem  23701  nconnsubb  23741  pthaus  23957  txhaus  23966  xkohaus  23972  regr1lem  24058  isust  24523  ustuqtop4  24563  methaus  24839  metnrmlem3  25181  iscau4  25600  pmltpclem1  25769  dvfsumlem2  26347  aannenlem1  26655  aannenlem2  26656  brslts  28148  bdayfinbndlem1  28853  istrkgcb  28918  hlbtwn  29077  iscgra  29316  dfcgra2  29338  f1otrge  29449  axlowdim  29539  axeuclidlem  29540  eengtrkg  29564  clwwlk  30574  upgr3v3e3cycl  30781  upgr4cycl4dv4e  30786  numclwwlk5  30989  ex-opab  31033  l2p  31081  vciOLD  31163  isvclem  31179  isnvlem  31212  dipass  31447  adj1  32535  adjeq  32537  cnlnssadj  32682  br8d  33202  dvdsruasso2  33941  dfufd2lem  34081  constrsuc  34370  constrconj  34377  constrllcllem  34384  constrcbvlem  34387  carsgmon  34946  carsgsigalem  34947  carsgclctunlem2  34951  carsgclctun  34953  bnj1154  35629  onprcf1acwevdlem1  35895  br8  36521  br6  36522  br4  36523  fvtransport  36797  brcgr3  36811  brfs  36844  fscgr  36845  btwnconn1lem11  36862  brsegle  36873  fvray  36906  linedegen  36908  fvline  36909  cbvproddavw  37069  bj-isclm  38212  poimirlem28  38566  poimirlem32  38570  heiborlem2  38746  hlsuprexch  40438  3dim1lem5  40523  lplni2  40594  2llnjN  40624  lvoli2  40638  2lplnj  40677  cdleme18d  41352  cdlemg1cex  41645  ismrc  43711  monotoddzzfi  43948  oddcomabszz  43950  zindbi  43952  rmydioph  44020  nnoeomeqom  44313  rp-brsslt  44423  fsumiunss  46586  sumnnodd  46641  stoweidlem31  47040  stoweidlem34  47043  stoweidlem43  47052  stoweidlem48  47057  fourierdlem42  47158  sge0iunmptlemre  47424  sge0iunmpt  47427  vonioo  47691  vonicc  47694  fundcmpsurinjpreimafv  48489  upgrimpths  49006  cycl3grtri  49044  grimgrtri  49046  usgrgrtrirex  49047  grlimgrtri  49100  sepfsepc  50035  iscnrm3rlem8  50054  iscnrm3llem2  50057