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  7203  xpord2lem  8072  xpord3lem  8079  frecseq123  8212  oeeui  8517  sbthfi  9108  pwfseqlem4a  10552  pwfseqlem4  10553  pfxccatin12lem3  14639  prodeq2w  15817  prodeq2ii  15818  prodeq2sdv  15830  divalg  16314  dfgcd2  16457  iscatd2  17587  posi  18223  issubg3  19057  pmtrfrn  19370  psgnunilem2  19407  psgnunilem3  19408  lmhmpropd  21007  lbsacsbs  21093  frlmphl  21718  neiptoptop  23046  neiptopnei  23047  cnhaus  23269  nrmsep  23272  dishaus  23297  ordthauslem  23298  nconnsubb  23338  pthaus  23553  txhaus  23562  xkohaus  23568  regr1lem  23654  isust  24119  ustuqtop4  24159  methaus  24435  metnrmlem3  24777  iscau4  25206  pmltpclem1  25376  dvfsumlem2  25960  dvfsumlem2OLD  25961  aannenlem1  26263  aannenlem2  26264  brsslt  27725  istrkgcb  28434  hlbtwn  28589  iscgra  28787  dfcgra2  28808  f1otrge  28850  axlowdim  28939  axeuclidlem  28940  eengtrkg  28964  clwwlk  29963  upgr3v3e3cycl  30160  upgr4cycl4dv4e  30165  numclwwlk5  30368  ex-opab  30412  l2p  30459  vciOLD  30541  isvclem  30557  isnvlem  30590  dipass  30825  adj1  31913  adjeq  31915  cnlnssadj  32060  br8d  32591  dvdsruasso2  33351  dfufd2lem  33514  constrsuc  33751  constrconj  33758  constrllcllem  33765  constrcbvlem  33768  carsgmon  34327  carsgsigalem  34328  carsgclctunlem2  34332  carsgclctun  34334  bnj1154  35011  br8  35800  br6  35801  br4  35802  fvtransport  36076  brcgr3  36090  brfs  36123  fscgr  36124  btwnconn1lem11  36141  brsegle  36152  fvray  36185  linedegen  36187  fvline  36188  cbvproddavw  36324  bj-isclm  37335  poimirlem28  37698  poimirlem32  37702  heiborlem2  37862  hlsuprexch  39490  3dim1lem5  39575  lplni2  39646  2llnjN  39676  lvoli2  39690  2lplnj  39729  cdleme18d  40404  cdlemg1cex  40697  ismrc  42804  monotoddzzfi  43045  oddcomabszz  43047  zindbi  43049  rmydioph  43117  nnoeomeqom  43415  rp-brsslt  43526  fsumiunss  45685  sumnnodd  45740  stoweidlem31  46139  stoweidlem34  46142  stoweidlem43  46151  stoweidlem48  46156  fourierdlem42  46257  sge0iunmptlemre  46523  sge0iunmpt  46526  vonioo  46790  vonicc  46793  fundcmpsurinjpreimafv  47518  upgrimpths  48019  cycl3grtri  48057  grimgrtri  48059  usgrgrtrirex  48060  grlimgrtri  48113  sepfsepc  49038  iscnrm3rlem8  49057  iscnrm3llem2  49060