Theorem 3anbi23d 1435

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  f1dom3el3dif  7021  wrecseq123  7942  oeeui  8222  fpwwe2lem5  10050  pwfseqlem4a  10077  pwfseqlem4  10078  pfxccatin12lem3  14088  prodeq2w  15260  prodeq2ii  15261  divalg  15748  dfgcd2  15888  iscatd2  16946  posi  17554  issubg3  18291  pmtrfrn  18580  psgnunilem2  18617  psgnunilem3  18618  lmhmpropd  19839  lbsacsbs  19922  frlmphl  20919  neiptoptop  21733  neiptopnei  21734  cnhaus  21956  nrmsep  21959  dishaus  21984  ordthauslem  21985  nconnsubb  22025  pthaus  22240  txhaus  22249  xkohaus  22255  regr1lem  22341  isust  22806  ustuqtop4  22847  methaus  23124  metnrmlem3  23463  iscau4  23876  pmltpclem1  24043  dvfsumlem2  24618  aannenlem1  24911  aannenlem2  24912  istrkgcb  26236  hlbtwn  26391  iscgra  26589  dfcgra2  26610  f1otrge  26652  axlowdim  26741  axeuclidlem  26742  eengtrkg  26766  clwwlk  27755  upgr3v3e3cycl  27953  upgr4cycl4dv4e  27958  numclwwlk5  28161  ex-opab  28205  l2p  28250  vciOLD  28332  isvclem  28348  isnvlem  28381  dipass  28616  adj1  29704  adjeq  29706  cnlnssadj  29851  br8d  30355  carsgmon  31567  carsgsigalem  31568  carsgclctunlem2  31572  carsgclctun  31574  bnj1154  32266  br8  32987  br6  32988  br4  32989  frecseq123  33114  brsslt  33249  fvtransport  33488  brcgr3  33502  brfs  33535  fscgr  33536  btwnconn1lem11  33553  brsegle  33564  fvray  33597  linedegen  33599  fvline  33600  bj-isclm  34566  poimirlem28  34914  poimirlem32  34918  heiborlem2  35084  hlsuprexch  36511  3dim1lem5  36596  lplni2  36667  2llnjN  36697  lvoli2  36711  2lplnj  36750  cdleme18d  37425  cdlemg1cex  37718  ismrc  39291  monotoddzzfi  39532  oddcomabszz  39534  zindbi  39536  rmydioph  39604  fsumiunss  41848  sumnnodd  41903  stoweidlem31  42309  stoweidlem34  42312  stoweidlem43  42321  stoweidlem48  42326  fourierdlem42  42427  sge0iunmptlemre  42690  sge0iunmpt  42693  vonioo  42957  vonicc  42960  fundcmpsurinjpreimafv  43561