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 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  f1dom3el3dif  7289  xpord2lem  8167  xpord3lem  8174  frecseq123  8307  wrecseq123OLD  8340  oeeui  8640  sbthfi  9239  pwfseqlem4a  10701  pwfseqlem4  10702  pfxccatin12lem3  14770  prodeq2w  15946  prodeq2ii  15947  prodeq2sdv  15959  divalg  16440  dfgcd2  16583  iscatd2  17724  posi  18363  issubg3  19162  pmtrfrn  19476  psgnunilem2  19513  psgnunilem3  19514  lmhmpropd  21072  lbsacsbs  21158  frlmphl  21801  neiptoptop  23139  neiptopnei  23140  cnhaus  23362  nrmsep  23365  dishaus  23390  ordthauslem  23391  nconnsubb  23431  pthaus  23646  txhaus  23655  xkohaus  23661  regr1lem  23747  isust  24212  ustuqtop4  24253  methaus  24533  metnrmlem3  24883  iscau4  25313  pmltpclem1  25483  dvfsumlem2  26067  dvfsumlem2OLD  26068  aannenlem1  26370  aannenlem2  26371  brsslt  27830  istrkgcb  28464  hlbtwn  28619  iscgra  28817  dfcgra2  28838  f1otrge  28880  axlowdim  28976  axeuclidlem  28977  eengtrkg  29001  clwwlk  30002  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  numclwwlk5  30407  ex-opab  30451  l2p  30498  vciOLD  30580  isvclem  30596  isnvlem  30629  dipass  30864  adj1  31952  adjeq  31954  cnlnssadj  32099  br8d  32622  dvdsruasso2  33414  dfufd2lem  33577  constrsuc  33779  constrconj  33786  carsgmon  34316  carsgsigalem  34317  carsgclctunlem2  34321  carsgclctun  34323  bnj1154  35013  br8  35756  br6  35757  br4  35758  fvtransport  36033  brcgr3  36047  brfs  36080  fscgr  36081  btwnconn1lem11  36098  brsegle  36109  fvray  36142  linedegen  36144  fvline  36145  cbvproddavw  36281  bj-isclm  37292  poimirlem28  37655  poimirlem32  37659  heiborlem2  37819  hlsuprexch  39383  3dim1lem5  39468  lplni2  39539  2llnjN  39569  lvoli2  39583  2lplnj  39622  cdleme18d  40297  cdlemg1cex  40590  ismrc  42712  monotoddzzfi  42954  oddcomabszz  42956  zindbi  42958  rmydioph  43026  nnoeomeqom  43325  rp-brsslt  43436  fsumiunss  45590  sumnnodd  45645  stoweidlem31  46046  stoweidlem34  46049  stoweidlem43  46058  stoweidlem48  46063  fourierdlem42  46164  sge0iunmptlemre  46430  sge0iunmpt  46433  vonioo  46697  vonicc  46700  fundcmpsurinjpreimafv  47395  cycl3grtri  47914  grimgrtri  47916  usgrgrtrirex  47917  grlimgrtri  47963  sepfsepc  48825  iscnrm3rlem8  48844  iscnrm3llem2  48847