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 261	. 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 397  df-3an 1089

This theorem is referenced by:  f1dom3el3dif  7270  xpord2lem  8130  xpord3lem  8137  frecseq123  8269  wrecseq123OLD  8302  oeeui  8604  sbthfi  9204  fpwwe2lem4  10631  pwfseqlem4a  10658  pwfseqlem4  10659  pfxccatin12lem3  14684  prodeq2w  15858  prodeq2ii  15859  divalg  16348  dfgcd2  16490  iscatd2  17627  posi  18272  issubg3  19026  pmtrfrn  19328  psgnunilem2  19365  psgnunilem3  19366  lmhmpropd  20689  lbsacsbs  20775  frlmphl  21342  neiptoptop  22642  neiptopnei  22643  cnhaus  22865  nrmsep  22868  dishaus  22893  ordthauslem  22894  nconnsubb  22934  pthaus  23149  txhaus  23158  xkohaus  23164  regr1lem  23250  isust  23715  ustuqtop4  23756  methaus  24036  metnrmlem3  24384  iscau4  24803  pmltpclem1  24972  dvfsumlem2  25551  aannenlem1  25848  aannenlem2  25849  brsslt  27294  istrkgcb  27745  hlbtwn  27900  iscgra  28098  dfcgra2  28119  f1otrge  28161  axlowdim  28257  axeuclidlem  28258  eengtrkg  28282  clwwlk  29274  upgr3v3e3cycl  29471  upgr4cycl4dv4e  29476  numclwwlk5  29679  ex-opab  29723  l2p  29770  vciOLD  29852  isvclem  29868  isnvlem  29901  dipass  30136  adj1  31224  adjeq  31226  cnlnssadj  31371  br8d  31877  carsgmon  33382  carsgsigalem  33383  carsgclctunlem2  33387  carsgclctun  33389  bnj1154  34079  br8  34795  br6  34796  br4  34797  fvtransport  35073  brcgr3  35087  brfs  35120  fscgr  35121  btwnconn1lem11  35138  brsegle  35149  fvray  35182  linedegen  35184  fvline  35185  gg-dvfsumlem2  35252  bj-isclm  36258  poimirlem28  36602  poimirlem32  36606  heiborlem2  36766  hlsuprexch  38338  3dim1lem5  38423  lplni2  38494  2llnjN  38524  lvoli2  38538  2lplnj  38577  cdleme18d  39252  cdlemg1cex  39545  ismrc  41521  monotoddzzfi  41763  oddcomabszz  41765  zindbi  41767  rmydioph  41835  nnoeomeqom  42144  rp-brsslt  42256  fsumiunss  44370  sumnnodd  44425  stoweidlem31  44826  stoweidlem34  44829  stoweidlem43  44838  stoweidlem48  44843  fourierdlem42  44944  sge0iunmptlemre  45210  sge0iunmpt  45213  vonioo  45477  vonicc  45480  fundcmpsurinjpreimafv  46155  sepfsepc  47638  iscnrm3rlem8  47658  iscnrm3llem2  47661