Theorem 3anbi23d 1439

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  f1dom3el3dif  7306  xpord2lem  8183  xpord3lem  8190  frecseq123  8323  wrecseq123OLD  8356  oeeui  8658  sbthfi  9265  pwfseqlem4a  10730  pwfseqlem4  10731  pfxccatin12lem3  14780  prodeq2w  15958  prodeq2ii  15959  prodeq2sdv  15971  divalg  16451  dfgcd2  16593  iscatd2  17739  posi  18387  issubg3  19184  pmtrfrn  19500  psgnunilem2  19537  psgnunilem3  19538  lmhmpropd  21095  lbsacsbs  21181  frlmphl  21824  neiptoptop  23160  neiptopnei  23161  cnhaus  23383  nrmsep  23386  dishaus  23411  ordthauslem  23412  nconnsubb  23452  pthaus  23667  txhaus  23676  xkohaus  23682  regr1lem  23768  isust  24233  ustuqtop4  24274  methaus  24554  metnrmlem3  24902  iscau4  25332  pmltpclem1  25502  dvfsumlem2  26087  dvfsumlem2OLD  26088  aannenlem1  26388  aannenlem2  26389  brsslt  27848  istrkgcb  28482  hlbtwn  28637  iscgra  28835  dfcgra2  28856  f1otrge  28898  axlowdim  28994  axeuclidlem  28995  eengtrkg  29019  clwwlk  30015  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  numclwwlk5  30420  ex-opab  30464  l2p  30511  vciOLD  30593  isvclem  30609  isnvlem  30642  dipass  30877  adj1  31965  adjeq  31967  cnlnssadj  32112  br8d  32632  dvdsruasso2  33379  dfufd2lem  33542  constrsuc  33728  constrconj  33735  carsgmon  34279  carsgsigalem  34280  carsgclctunlem2  34284  carsgclctun  34286  bnj1154  34975  br8  35718  br6  35719  br4  35720  fvtransport  35996  brcgr3  36010  brfs  36043  fscgr  36044  btwnconn1lem11  36061  brsegle  36072  fvray  36105  linedegen  36107  fvline  36108  cbvproddavw  36246  bj-isclm  37257  poimirlem28  37608  poimirlem32  37612  heiborlem2  37772  hlsuprexch  39338  3dim1lem5  39423  lplni2  39494  2llnjN  39524  lvoli2  39538  2lplnj  39577  cdleme18d  40252  cdlemg1cex  40545  ismrc  42657  monotoddzzfi  42899  oddcomabszz  42901  zindbi  42903  rmydioph  42971  nnoeomeqom  43274  rp-brsslt  43385  fsumiunss  45496  sumnnodd  45551  stoweidlem31  45952  stoweidlem34  45955  stoweidlem43  45964  stoweidlem48  45969  fourierdlem42  46070  sge0iunmptlemre  46336  sge0iunmpt  46339  vonioo  46603  vonicc  46606  fundcmpsurinjpreimafv  47282  grimgrtri  47798  usgrgrtrirex  47799  grlimgrtri  47820  sepfsepc  48607  iscnrm3rlem8  48627  iscnrm3llem2  48630