Theorem 3anbi23d 1438

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  f1dom3el3dif  7139  frecseq123  8089  wrecseq123OLD  8122  oeeui  8418  sbthfi  8967  fpwwe2lem4  10391  pwfseqlem4a  10418  pwfseqlem4  10419  pfxccatin12lem3  14443  prodeq2w  15620  prodeq2ii  15621  divalg  16110  dfgcd2  16252  iscatd2  17388  posi  18033  issubg3  18771  pmtrfrn  19064  psgnunilem2  19101  psgnunilem3  19102  lmhmpropd  20333  lbsacsbs  20416  frlmphl  20986  neiptoptop  22280  neiptopnei  22281  cnhaus  22503  nrmsep  22506  dishaus  22531  ordthauslem  22532  nconnsubb  22572  pthaus  22787  txhaus  22796  xkohaus  22802  regr1lem  22888  isust  23353  ustuqtop4  23394  methaus  23674  metnrmlem3  24022  iscau4  24441  pmltpclem1  24610  dvfsumlem2  25189  aannenlem1  25486  aannenlem2  25487  istrkgcb  26815  hlbtwn  26970  iscgra  27168  dfcgra2  27189  f1otrge  27231  axlowdim  27327  axeuclidlem  27328  eengtrkg  27352  clwwlk  28343  upgr3v3e3cycl  28540  upgr4cycl4dv4e  28545  numclwwlk5  28748  ex-opab  28792  l2p  28837  vciOLD  28919  isvclem  28935  isnvlem  28968  dipass  29203  adj1  30291  adjeq  30293  cnlnssadj  30438  br8d  30946  carsgmon  32277  carsgsigalem  32278  carsgclctunlem2  32282  carsgclctun  32284  bnj1154  32975  br8  33719  br6  33720  br4  33721  xpord2lem  33785  xpord3lem  33791  brsslt  33976  fvtransport  34330  brcgr3  34344  brfs  34377  fscgr  34378  btwnconn1lem11  34395  brsegle  34406  fvray  34439  linedegen  34441  fvline  34442  bj-isclm  35458  poimirlem28  35801  poimirlem32  35805  heiborlem2  35966  hlsuprexch  37391  3dim1lem5  37476  lplni2  37547  2llnjN  37577  lvoli2  37591  2lplnj  37630  cdleme18d  38305  cdlemg1cex  38598  ismrc  40520  monotoddzzfi  40761  oddcomabszz  40763  zindbi  40765  rmydioph  40833  fsumiunss  43087  sumnnodd  43142  stoweidlem31  43543  stoweidlem34  43546  stoweidlem43  43555  stoweidlem48  43560  fourierdlem42  43661  sge0iunmptlemre  43924  sge0iunmpt  43927  vonioo  44191  vonicc  44194  fundcmpsurinjpreimafv  44829  sepfsepc  46190  iscnrm3rlem8  46210  iscnrm3llem2  46213