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 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  7215  xpord2lem  8084  xpord3lem  8091  frecseq123  8224  oeeui  8530  sbthfi  9123  pwfseqlem4a  10572  pwfseqlem4  10573  pfxccatin12lem3  14655  prodeq2w  15833  prodeq2ii  15834  prodeq2sdv  15846  divalg  16330  dfgcd2  16473  iscatd2  17604  posi  18240  issubg3  19074  pmtrfrn  19387  psgnunilem2  19424  psgnunilem3  19425  lmhmpropd  21025  lbsacsbs  21111  frlmphl  21736  neiptoptop  23075  neiptopnei  23076  cnhaus  23298  nrmsep  23301  dishaus  23326  ordthauslem  23327  nconnsubb  23367  pthaus  23582  txhaus  23591  xkohaus  23597  regr1lem  23683  isust  24148  ustuqtop4  24188  methaus  24464  metnrmlem3  24806  iscau4  25235  pmltpclem1  25405  dvfsumlem2  25989  dvfsumlem2OLD  25990  aannenlem1  26292  aannenlem2  26293  brslts  27758  bdayfinbndlem1  28463  istrkgcb  28528  hlbtwn  28683  iscgra  28881  dfcgra2  28902  f1otrge  28944  axlowdim  29034  axeuclidlem  29035  eengtrkg  29059  clwwlk  30058  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  numclwwlk5  30463  ex-opab  30507  l2p  30554  vciOLD  30636  isvclem  30652  isnvlem  30685  dipass  30920  adj1  32008  adjeq  32010  cnlnssadj  32155  br8d  32686  dvdsruasso2  33467  dfufd2lem  33630  constrsuc  33895  constrconj  33902  constrllcllem  33909  constrcbvlem  33912  carsgmon  34471  carsgsigalem  34472  carsgclctunlem2  34476  carsgclctun  34478  bnj1154  35155  br8  35950  br6  35951  br4  35952  fvtransport  36226  brcgr3  36240  brfs  36273  fscgr  36274  btwnconn1lem11  36291  brsegle  36302  fvray  36335  linedegen  36337  fvline  36338  cbvproddavw  36474  bj-isclm  37496  poimirlem28  37849  poimirlem32  37853  heiborlem2  38013  hlsuprexch  39651  3dim1lem5  39736  lplni2  39807  2llnjN  39837  lvoli2  39851  2lplnj  39890  cdleme18d  40565  cdlemg1cex  40858  ismrc  42953  monotoddzzfi  43194  oddcomabszz  43196  zindbi  43198  rmydioph  43266  nnoeomeqom  43564  rp-brsslt  43674  fsumiunss  45831  sumnnodd  45886  stoweidlem31  46285  stoweidlem34  46288  stoweidlem43  46297  stoweidlem48  46302  fourierdlem42  46403  sge0iunmptlemre  46669  sge0iunmpt  46672  vonioo  46936  vonicc  46939  fundcmpsurinjpreimafv  47664  upgrimpths  48165  cycl3grtri  48203  grimgrtri  48205  usgrgrtrirex  48206  grlimgrtri  48259  sepfsepc  49183  iscnrm3rlem8  49202  iscnrm3llem2  49205