Theorem 3anbi23d 1441

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  f1dom3el3dif  7247  xpord2lem  8124  xpord3lem  8131  frecseq123  8264  oeeui  8569  sbthfi  9169  pwfseqlem4a  10621  pwfseqlem4  10622  pfxccatin12lem3  14704  prodeq2w  15883  prodeq2ii  15884  prodeq2sdv  15896  divalg  16380  dfgcd2  16523  iscatd2  17649  posi  18285  issubg3  19083  pmtrfrn  19395  psgnunilem2  19432  psgnunilem3  19433  lmhmpropd  20987  lbsacsbs  21073  frlmphl  21697  neiptoptop  23025  neiptopnei  23026  cnhaus  23248  nrmsep  23251  dishaus  23276  ordthauslem  23277  nconnsubb  23317  pthaus  23532  txhaus  23541  xkohaus  23547  regr1lem  23633  isust  24098  ustuqtop4  24139  methaus  24415  metnrmlem3  24757  iscau4  25186  pmltpclem1  25356  dvfsumlem2  25940  dvfsumlem2OLD  25941  aannenlem1  26243  aannenlem2  26244  brsslt  27704  istrkgcb  28390  hlbtwn  28545  iscgra  28743  dfcgra2  28764  f1otrge  28806  axlowdim  28895  axeuclidlem  28896  eengtrkg  28920  clwwlk  29919  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  numclwwlk5  30324  ex-opab  30368  l2p  30415  vciOLD  30497  isvclem  30513  isnvlem  30546  dipass  30781  adj1  31869  adjeq  31871  cnlnssadj  32016  br8d  32545  dvdsruasso2  33364  dfufd2lem  33527  constrsuc  33735  constrconj  33742  constrllcllem  33749  constrcbvlem  33752  carsgmon  34312  carsgsigalem  34313  carsgclctunlem2  34317  carsgclctun  34319  bnj1154  34996  br8  35750  br6  35751  br4  35752  fvtransport  36027  brcgr3  36041  brfs  36074  fscgr  36075  btwnconn1lem11  36092  brsegle  36103  fvray  36136  linedegen  36138  fvline  36139  cbvproddavw  36275  bj-isclm  37286  poimirlem28  37649  poimirlem32  37653  heiborlem2  37813  hlsuprexch  39382  3dim1lem5  39467  lplni2  39538  2llnjN  39568  lvoli2  39582  2lplnj  39621  cdleme18d  40296  cdlemg1cex  40589  ismrc  42696  monotoddzzfi  42938  oddcomabszz  42940  zindbi  42942  rmydioph  43010  nnoeomeqom  43308  rp-brsslt  43419  fsumiunss  45580  sumnnodd  45635  stoweidlem31  46036  stoweidlem34  46039  stoweidlem43  46048  stoweidlem48  46053  fourierdlem42  46154  sge0iunmptlemre  46420  sge0iunmpt  46423  vonioo  46687  vonicc  46690  fundcmpsurinjpreimafv  47413  upgrimpths  47913  cycl3grtri  47950  grimgrtri  47952  usgrgrtrirex  47953  grlimgrtri  47999  sepfsepc  48920  iscnrm3rlem8  48939  iscnrm3llem2  48942