Theorem 3anbi23d 1442

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ w3a 1054

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  f1dom3el3dif  6566  wrecseq123  7453  oeeui  7727  fpwwe2lem5  9494  pwfseqlem4a  9521  pwfseqlem4  9522  swrdccatin12lem3  13536  prodeq2w  14686  prodeq2ii  14687  divalg  15173  dfgcd2  15310  iscatd2  16389  posi  16997  issubg3  17659  pmtrfrn  17924  psgnunilem2  17961  psgnunilem3  17962  lmhmpropd  19121  lbsacsbs  19204  frlmphl  20168  neiptoptop  20983  neiptopnei  20984  cnhaus  21206  nrmsep  21209  dishaus  21234  ordthauslem  21235  nconnsubb  21274  pthaus  21489  txhaus  21498  xkohaus  21504  regr1lem  21590  isust  22054  ustuqtop4  22095  methaus  22372  metnrmlem3  22711  iscau4  23123  pmltpclem1  23263  dvfsumlem2  23835  aannenlem1  24128  aannenlem2  24129  istrkgcb  25400  hlbtwn  25551  iscgra  25746  dfcgra2  25766  f1otrge  25797  axlowdim  25886  axeuclidlem  25887  eengtrkg  25910  clwwlk  26951  clwlksfclwwlk  27049  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  numclwwlk5  27375  ex-opab  27419  l2p  27461  vciOLD  27544  isvclem  27560  isnvlem  27593  dipass  27828  adj1  28920  adjeq  28922  cnlnssadj  29067  br8d  29548  carsgmon  30504  carsgsigalem  30505  carsgclctunlem2  30509  carsgclctun  30511  bnj1154  31193  br8  31772  br6  31773  br4  31774  frecseq123  31902  brsslt  32025  fvtransport  32264  brcgr3  32278  brfs  32311  fscgr  32312  btwnconn1lem11  32329  brsegle  32340  fvray  32373  linedegen  32375  fvline  32376  poimirlem28  33567  poimirlem32  33571  heiborlem2  33741  hlsuprexch  34985  3dim1lem5  35070  lplni2  35141  2llnjN  35171  lvoli2  35185  2lplnj  35224  cdleme18d  35900  cdlemg1cex  36193  ismrc  37581  monotoddzzfi  37824  oddcomabszz  37826  zindbi  37828  rmydioph  37898  fsumiunss  40125  sumnnodd  40180  stoweidlem31  40566  stoweidlem34  40569  stoweidlem43  40578  stoweidlem48  40583  fourierdlem42  40684  sge0iunmptlemre  40950  sge0iunmpt  40953  vonioo  41217  vonicc  41220