Theorem 3anbi23d 1467

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  f1dom3el3dif  7272  xpord2lem  8144  xpord3lem  8151  frecseq123  8285  oeeui  8594  sbthfi  9190  pwfseqlem4a  10663  pwfseqlem4  10664  pfxccatin12lem3  14793  prodeq2w  15989  prodeq2ii  15990  prodeq2sdv  16002  divalg  16485  dfgcd2  16628  iscatd2  17761  posi  18397  issubg3  19257  pmtrfrn  19574  psgnunilem2  19611  psgnunilem3  19612  lmhmpropd  21246  lbsacsbs  21332  frlmphl  21983  neiptoptop  23340  neiptopnei  23341  cnhaus  23563  nrmsep  23566  dishaus  23591  ordthauslem  23592  nconnsubb  23632  pthaus  23848  txhaus  23857  xkohaus  23863  regr1lem  23949  isust  24414  ustuqtop4  24454  methaus  24730  metnrmlem3  25072  iscau4  25491  pmltpclem1  25660  dvfsumlem2  26239  aannenlem1  26544  aannenlem2  26545  brslts  28008  bdayfinbndlem1  28713  istrkgcb  28778  hlbtwn  28936  iscgra  29173  dfcgra2  29194  f1otrge  29278  axlowdim  29368  axeuclidlem  29369  eengtrkg  29393  clwwlk  30403  upgr3v3e3cycl  30604  upgr4cycl4dv4e  30609  numclwwlk5  30812  ex-opab  30856  l2p  30904  vciOLD  30986  isvclem  31002  isnvlem  31035  dipass  31270  adj1  32358  adjeq  32360  cnlnssadj  32505  br8d  33026  dvdsruasso2  33765  dfufd2lem  33905  constrsuc  34194  constrconj  34201  constrllcllem  34208  constrcbvlem  34211  carsgmon  34771  carsgsigalem  34772  carsgclctunlem2  34776  carsgclctun  34778  bnj1154  35454  br8  36287  br6  36288  br4  36289  fvtransport  36563  brcgr3  36577  brfs  36610  fscgr  36611  btwnconn1lem11  36628  brsegle  36639  fvray  36672  linedegen  36674  fvline  36675  cbvproddavw  36851  bj-isclm  37994  poimirlem28  38358  poimirlem32  38362  heiborlem2  38523  hlsuprexch  40215  3dim1lem5  40300  lplni2  40371  2llnjN  40401  lvoli2  40415  2lplnj  40454  cdleme18d  41129  cdlemg1cex  41422  ismrc  43492  monotoddzzfi  43729  oddcomabszz  43731  zindbi  43733  rmydioph  43801  nnoeomeqom  44099  rp-brsslt  44209  fsumiunss  46351  sumnnodd  46406  stoweidlem31  46805  stoweidlem34  46808  stoweidlem43  46817  stoweidlem48  46822  fourierdlem42  46923  sge0iunmptlemre  47189  sge0iunmpt  47192  vonioo  47456  vonicc  47459  fundcmpsurinjpreimafv  48217  upgrimpths  48734  cycl3grtri  48772  grimgrtri  48774  usgrgrtrirex  48775  grlimgrtri  48828  sepfsepc  49765  iscnrm3rlem8  49784  iscnrm3llem2  49787