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 262	. 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂))
2		3anbi12d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3		3anbi12d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	1, 2, 3	3anbi123d 1435	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  7288  xpord2lem  8165  xpord3lem  8172  frecseq123  8305  wrecseq123OLD  8338  oeeui  8638  sbthfi  9236  pwfseqlem4a  10698  pwfseqlem4  10699  pfxccatin12lem3  14766  prodeq2w  15942  prodeq2ii  15943  prodeq2sdv  15955  divalg  16436  dfgcd2  16579  iscatd2  17725  posi  18374  issubg3  19174  pmtrfrn  19490  psgnunilem2  19527  psgnunilem3  19528  lmhmpropd  21089  lbsacsbs  21175  frlmphl  21818  neiptoptop  23154  neiptopnei  23155  cnhaus  23377  nrmsep  23380  dishaus  23405  ordthauslem  23406  nconnsubb  23446  pthaus  23661  txhaus  23670  xkohaus  23676  regr1lem  23762  isust  24227  ustuqtop4  24268  methaus  24548  metnrmlem3  24896  iscau4  25326  pmltpclem1  25496  dvfsumlem2  26081  dvfsumlem2OLD  26082  aannenlem1  26384  aannenlem2  26385  brsslt  27844  istrkgcb  28478  hlbtwn  28633  iscgra  28831  dfcgra2  28852  f1otrge  28894  axlowdim  28990  axeuclidlem  28991  eengtrkg  29015  clwwlk  30011  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  numclwwlk5  30416  ex-opab  30460  l2p  30507  vciOLD  30589  isvclem  30605  isnvlem  30638  dipass  30873  adj1  31961  adjeq  31963  cnlnssadj  32108  br8d  32629  dvdsruasso2  33393  dfufd2lem  33556  constrsuc  33742  constrconj  33749  carsgmon  34295  carsgsigalem  34296  carsgclctunlem2  34300  carsgclctun  34302  bnj1154  34991  br8  35735  br6  35736  br4  35737  fvtransport  36013  brcgr3  36027  brfs  36060  fscgr  36061  btwnconn1lem11  36078  brsegle  36089  fvray  36122  linedegen  36124  fvline  36125  cbvproddavw  36262  bj-isclm  37273  poimirlem28  37634  poimirlem32  37638  heiborlem2  37798  hlsuprexch  39363  3dim1lem5  39448  lplni2  39519  2llnjN  39549  lvoli2  39563  2lplnj  39602  cdleme18d  40277  cdlemg1cex  40570  ismrc  42688  monotoddzzfi  42930  oddcomabszz  42932  zindbi  42934  rmydioph  43002  nnoeomeqom  43301  rp-brsslt  43412  fsumiunss  45530  sumnnodd  45585  stoweidlem31  45986  stoweidlem34  45989  stoweidlem43  45998  stoweidlem48  46003  fourierdlem42  46104  sge0iunmptlemre  46370  sge0iunmpt  46373  vonioo  46637  vonicc  46640  fundcmpsurinjpreimafv  47332  grimgrtri  47851  usgrgrtrirex  47852  grlimgrtri  47898  sepfsepc  48723  iscnrm3rlem8  48743  iscnrm3llem2  48746