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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  f1dom3el3dif  7267  xpord2lem  8134  xpord3lem  8141  frecseq123  8275  oeeui  8584  sbthfi  9179  pwfseqlem4a  10641  pwfseqlem4  10642  pfxccatin12lem3  14765  prodeq2w  15960  prodeq2ii  15961  prodeq2sdv  15973  divalg  16456  dfgcd2  16599  iscatd2  17732  posi  18368  issubg3  19206  pmtrfrn  19523  psgnunilem2  19560  psgnunilem3  19561  lmhmpropd  21194  lbsacsbs  21280  frlmphl  21931  neiptoptop  23288  neiptopnei  23289  cnhaus  23511  nrmsep  23514  dishaus  23539  ordthauslem  23540  nconnsubb  23580  pthaus  23795  txhaus  23804  xkohaus  23810  regr1lem  23896  isust  24361  ustuqtop4  24401  methaus  24677  metnrmlem3  25019  iscau4  25438  pmltpclem1  25607  dvfsumlem2  26186  aannenlem1  26491  aannenlem2  26492  brslts  27955  bdayfinbndlem1  28660  istrkgcb  28725  hlbtwn  28883  iscgra  29120  dfcgra2  29141  f1otrge  29221  axlowdim  29311  axeuclidlem  29312  eengtrkg  29336  clwwlk  30334  upgr3v3e3cycl  30531  upgr4cycl4dv4e  30536  numclwwlk5  30739  ex-opab  30783  l2p  30831  vciOLD  30913  isvclem  30929  isnvlem  30962  dipass  31197  adj1  32285  adjeq  32287  cnlnssadj  32432  br8d  32953  dvdsruasso2  33699  dfufd2lem  33839  constrsuc  34128  constrconj  34135  constrllcllem  34142  constrcbvlem  34145  carsgmon  34704  carsgsigalem  34705  carsgclctunlem2  34709  carsgclctun  34711  bnj1154  35387  br8  36248  br6  36249  br4  36250  fvtransport  36524  brcgr3  36538  brfs  36571  fscgr  36572  btwnconn1lem11  36589  brsegle  36600  fvray  36633  linedegen  36635  fvline  36636  cbvproddavw  36812  bj-isclm  37955  poimirlem28  38319  poimirlem32  38323  heiborlem2  38483  hlsuprexch  40175  3dim1lem5  40260  lplni2  40331  2llnjN  40361  lvoli2  40375  2lplnj  40414  cdleme18d  41089  cdlemg1cex  41382  ismrc  43452  monotoddzzfi  43689  oddcomabszz  43691  zindbi  43693  rmydioph  43761  nnoeomeqom  44059  rp-brsslt  44169  fsumiunss  46311  sumnnodd  46366  stoweidlem31  46765  stoweidlem34  46768  stoweidlem43  46777  stoweidlem48  46782  fourierdlem42  46883  sge0iunmptlemre  47149  sge0iunmpt  47152  vonioo  47416  vonicc  47419  fundcmpsurinjpreimafv  48177  upgrimpths  48694  cycl3grtri  48732  grimgrtri  48734  usgrgrtrirex  48735  grlimgrtri  48788  sepfsepc  49726  iscnrm3rlem8  49745  iscnrm3llem2  49748