Theorem 3anbi23d 1435

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 264	. 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂))
2		3anbi12d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3		3anbi12d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	1, 2, 3	3anbi123d 1432	1 ⊢ (𝜑 → ((𝜂 ∧ 𝜓 ∧ 𝜃) ↔ (𝜂 ∧ 𝜒 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  f1dom3el3dif  7027  wrecseq123  7948  oeeui  8228  fpwwe2lem5  10056  pwfseqlem4a  10083  pwfseqlem4  10084  pfxccatin12lem3  14094  prodeq2w  15266  prodeq2ii  15267  divalg  15754  dfgcd2  15894  iscatd2  16952  posi  17560  issubg3  18297  pmtrfrn  18586  psgnunilem2  18623  psgnunilem3  18624  lmhmpropd  19845  lbsacsbs  19928  frlmphl  20925  neiptoptop  21739  neiptopnei  21740  cnhaus  21962  nrmsep  21965  dishaus  21990  ordthauslem  21991  nconnsubb  22031  pthaus  22246  txhaus  22255  xkohaus  22261  regr1lem  22347  isust  22812  ustuqtop4  22853  methaus  23130  metnrmlem3  23469  iscau4  23882  pmltpclem1  24049  dvfsumlem2  24624  aannenlem1  24917  aannenlem2  24918  istrkgcb  26242  hlbtwn  26397  iscgra  26595  dfcgra2  26616  f1otrge  26658  axlowdim  26747  axeuclidlem  26748  eengtrkg  26772  clwwlk  27761  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  numclwwlk5  28167  ex-opab  28211  l2p  28256  vciOLD  28338  isvclem  28354  isnvlem  28387  dipass  28622  adj1  29710  adjeq  29712  cnlnssadj  29857  br8d  30361  carsgmon  31572  carsgsigalem  31573  carsgclctunlem2  31577  carsgclctun  31579  bnj1154  32271  br8  32992  br6  32993  br4  32994  frecseq123  33119  brsslt  33254  fvtransport  33493  brcgr3  33507  brfs  33540  fscgr  33541  btwnconn1lem11  33558  brsegle  33569  fvray  33602  linedegen  33604  fvline  33605  bj-isclm  34575  poimirlem28  34935  poimirlem32  34939  heiborlem2  35105  hlsuprexch  36532  3dim1lem5  36617  lplni2  36688  2llnjN  36718  lvoli2  36732  2lplnj  36771  cdleme18d  37446  cdlemg1cex  37739  ismrc  39318  monotoddzzfi  39559  oddcomabszz  39561  zindbi  39563  rmydioph  39631  fsumiunss  41876  sumnnodd  41931  stoweidlem31  42336  stoweidlem34  42339  stoweidlem43  42348  stoweidlem48  42353  fourierdlem42  42454  sge0iunmptlemre  42717  sge0iunmpt  42720  vonioo  42984  vonicc  42987  fundcmpsurinjpreimafv  43588