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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  f1dom3el3dif  7267  xpord2lem  8141  xpord3lem  8148  frecseq123  8282  oeeui  8593  sbthfi  9196  pwfseqlem4a  10673  pwfseqlem4  10674  pfxccatin12lem3  14804  prodeq2w  16002  prodeq2ii  16003  prodeq2sdv  16014  divalg  16496  dfgcd2  16639  iscatd2  17772  posi  18408  issubg3  19271  pmtrfrn  19588  psgnunilem2  19625  psgnunilem3  19626  lmhmpropd  21260  lbsacsbs  21346  frlmphl  21997  neiptoptop  23359  neiptopnei  23360  cnhaus  23582  nrmsep  23585  dishaus  23610  ordthauslem  23611  nconnsubb  23651  pthaus  23867  txhaus  23876  xkohaus  23882  regr1lem  23968  isust  24433  ustuqtop4  24473  methaus  24749  metnrmlem3  25091  iscau4  25510  pmltpclem1  25679  dvfsumlem2  26257  aannenlem1  26567  aannenlem2  26568  brslts  28030  bdayfinbndlem1  28735  istrkgcb  28800  hlbtwn  28959  iscgra  29198  dfcgra2  29220  f1otrge  29331  axlowdim  29421  axeuclidlem  29422  eengtrkg  29446  clwwlk  30456  upgr3v3e3cycl  30663  upgr4cycl4dv4e  30668  numclwwlk5  30871  ex-opab  30915  l2p  30963  vciOLD  31045  isvclem  31061  isnvlem  31094  dipass  31329  adj1  32417  adjeq  32419  cnlnssadj  32564  br8d  33084  dvdsruasso2  33822  dfufd2lem  33962  constrsuc  34251  constrconj  34258  constrllcllem  34265  constrcbvlem  34268  carsgmon  34828  carsgsigalem  34829  carsgclctunlem2  34833  carsgclctun  34835  bnj1154  35511  br8  36338  br6  36339  br4  36340  fvtransport  36615  brcgr3  36629  brfs  36662  fscgr  36663  btwnconn1lem11  36680  brsegle  36691  fvray  36724  linedegen  36726  fvline  36727  cbvproddavw  36903  bj-isclm  38046  poimirlem28  38400  poimirlem32  38404  heiborlem2  38565  hlsuprexch  40257  3dim1lem5  40342  lplni2  40413  2llnjN  40443  lvoli2  40457  2lplnj  40496  cdleme18d  41171  cdlemg1cex  41464  ismrc  43549  monotoddzzfi  43786  oddcomabszz  43788  zindbi  43790  rmydioph  43858  nnoeomeqom  44156  rp-brsslt  44266  fsumiunss  46408  sumnnodd  46463  stoweidlem31  46862  stoweidlem34  46865  stoweidlem43  46874  stoweidlem48  46879  fourierdlem42  46980  sge0iunmptlemre  47246  sge0iunmpt  47249  vonioo  47513  vonicc  47516  fundcmpsurinjpreimafv  48311  upgrimpths  48828  cycl3grtri  48866  grimgrtri  48868  usgrgrtrirex  48869  grlimgrtri  48922  sepfsepc  49857  iscnrm3rlem8  49876  iscnrm3llem2  49879