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  7267  xpord2lem  8146  xpord3lem  8153  frecseq123  8286  wrecseq123OLD  8319  oeeui  8619  sbthfi  9218  pwfseqlem4a  10680  pwfseqlem4  10681  pfxccatin12lem3  14755  prodeq2w  15931  prodeq2ii  15932  prodeq2sdv  15944  divalg  16427  dfgcd2  16570  iscatd2  17698  posi  18334  issubg3  19132  pmtrfrn  19444  psgnunilem2  19481  psgnunilem3  19482  lmhmpropd  21036  lbsacsbs  21122  frlmphl  21746  neiptoptop  23074  neiptopnei  23075  cnhaus  23297  nrmsep  23300  dishaus  23325  ordthauslem  23326  nconnsubb  23366  pthaus  23581  txhaus  23590  xkohaus  23596  regr1lem  23682  isust  24147  ustuqtop4  24188  methaus  24464  metnrmlem3  24806  iscau4  25236  pmltpclem1  25406  dvfsumlem2  25990  dvfsumlem2OLD  25991  aannenlem1  26293  aannenlem2  26294  brsslt  27754  istrkgcb  28440  hlbtwn  28595  iscgra  28793  dfcgra2  28814  f1otrge  28856  axlowdim  28945  axeuclidlem  28946  eengtrkg  28970  clwwlk  29969  upgr3v3e3cycl  30166  upgr4cycl4dv4e  30171  numclwwlk5  30374  ex-opab  30418  l2p  30465  vciOLD  30547  isvclem  30563  isnvlem  30596  dipass  30831  adj1  31919  adjeq  31921  cnlnssadj  32066  br8d  32595  dvdsruasso2  33406  dfufd2lem  33569  constrsuc  33777  constrconj  33784  constrllcllem  33791  constrcbvlem  33794  carsgmon  34351  carsgsigalem  34352  carsgclctunlem2  34356  carsgclctun  34358  bnj1154  35035  br8  35778  br6  35779  br4  35780  fvtransport  36055  brcgr3  36069  brfs  36102  fscgr  36103  btwnconn1lem11  36120  brsegle  36131  fvray  36164  linedegen  36166  fvline  36167  cbvproddavw  36303  bj-isclm  37314  poimirlem28  37677  poimirlem32  37681  heiborlem2  37841  hlsuprexch  39405  3dim1lem5  39490  lplni2  39561  2llnjN  39591  lvoli2  39605  2lplnj  39644  cdleme18d  40319  cdlemg1cex  40612  ismrc  42691  monotoddzzfi  42933  oddcomabszz  42935  zindbi  42937  rmydioph  43005  nnoeomeqom  43303  rp-brsslt  43414  fsumiunss  45571  sumnnodd  45626  stoweidlem31  46027  stoweidlem34  46030  stoweidlem43  46039  stoweidlem48  46044  fourierdlem42  46145  sge0iunmptlemre  46411  sge0iunmpt  46414  vonioo  46678  vonicc  46681  fundcmpsurinjpreimafv  47389  upgrimpths  47889  cycl3grtri  47926  grimgrtri  47928  usgrgrtrirex  47929  grlimgrtri  47975  sepfsepc  48869  iscnrm3rlem8  48888  iscnrm3llem2  48891