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 205   ∧ 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 206  df-an 398  df-3an 1089

This theorem is referenced by:  f1dom3el3dif  7174  frecseq123  8129  wrecseq123OLD  8162  oeeui  8464  sbthfi  9023  fpwwe2lem4  10436  pwfseqlem4a  10463  pwfseqlem4  10464  pfxccatin12lem3  14490  prodeq2w  15667  prodeq2ii  15668  divalg  16157  dfgcd2  16299  iscatd2  17435  posi  18080  issubg3  18818  pmtrfrn  19111  psgnunilem2  19148  psgnunilem3  19149  lmhmpropd  20380  lbsacsbs  20463  frlmphl  21033  neiptoptop  22327  neiptopnei  22328  cnhaus  22550  nrmsep  22553  dishaus  22578  ordthauslem  22579  nconnsubb  22619  pthaus  22834  txhaus  22843  xkohaus  22849  regr1lem  22935  isust  23400  ustuqtop4  23441  methaus  23721  metnrmlem3  24069  iscau4  24488  pmltpclem1  24657  dvfsumlem2  25236  aannenlem1  25533  aannenlem2  25534  istrkgcb  26862  hlbtwn  27017  iscgra  27215  dfcgra2  27236  f1otrge  27278  axlowdim  27374  axeuclidlem  27375  eengtrkg  27399  clwwlk  28392  upgr3v3e3cycl  28589  upgr4cycl4dv4e  28594  numclwwlk5  28797  ex-opab  28841  l2p  28886  vciOLD  28968  isvclem  28984  isnvlem  29017  dipass  29252  adj1  30340  adjeq  30342  cnlnssadj  30487  br8d  30995  carsgmon  32326  carsgsigalem  32327  carsgclctunlem2  32331  carsgclctun  32333  bnj1154  33024  br8  33768  br6  33769  br4  33770  xpord2lem  33834  xpord3lem  33840  brsslt  34025  fvtransport  34379  brcgr3  34393  brfs  34426  fscgr  34427  btwnconn1lem11  34444  brsegle  34455  fvray  34488  linedegen  34490  fvline  34491  bj-isclm  35506  poimirlem28  35849  poimirlem32  35853  heiborlem2  36014  hlsuprexch  37437  3dim1lem5  37522  lplni2  37593  2llnjN  37623  lvoli2  37637  2lplnj  37676  cdleme18d  38351  cdlemg1cex  38644  ismrc  40560  monotoddzzfi  40802  oddcomabszz  40804  zindbi  40806  rmydioph  40874  fsumiunss  43165  sumnnodd  43220  stoweidlem31  43621  stoweidlem34  43624  stoweidlem43  43633  stoweidlem48  43638  fourierdlem42  43739  sge0iunmptlemre  44003  sge0iunmpt  44006  vonioo  44270  vonicc  44273  fundcmpsurinjpreimafv  44918  sepfsepc  46279  iscnrm3rlem8  46299  iscnrm3llem2  46302