Theorem 3anbi23d 1394

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  f1dom3el3dif  6426  wrecseq123  7295  oeeui  7569  fpwwe2lem5  9335  pwfseqlem4a  9362  pwfseqlem4  9363  swrdccatin12lem3  13341  prodeq2w  14481  prodeq2ii  14482  divalg  14964  dfgcd2  15101  iscatd2  16165  posi  16773  issubg3  17435  pmtrfrn  17701  psgnunilem2  17738  psgnunilem3  17739  lmhmpropd  18894  lbsacsbs  18977  frlmphl  19939  neiptoptop  20745  neiptopnei  20746  cnhaus  20968  nrmsep  20971  dishaus  20996  ordthauslem  20997  nconsubb  21036  pthaus  21251  txhaus  21260  xkohaus  21266  regr1lem  21352  isust  21817  ustuqtop4  21858  methaus  22135  metnrmlem3  22472  iscau4  22885  pmltpclem1  23024  dvfsumlem2  23594  aannenlem1  23887  aannenlem2  23888  istrkgcb  25155  hlbtwn  25306  iscgra  25501  dfcgra2  25521  f1otrge  25552  axlowdim  25641  axeuclidlem  25642  eengtrkg  25665  wlkelwrd  26058  wlkon  26061  3v3e3cycl1  26172  4cycl4v4e  26194  4cycl4dv4e  26196  clwlkfclwwlk  26371  numclwwlk5  26639  ex-opab  26681  vciOLD  26800  isvclem  26816  isnvlem  26849  dipass  27084  adj1  28176  adjeq  28178  cnlnssadj  28323  br8d  28802  carsgmon  29703  carsgsigalem  29704  carsgclctunlem2  29708  carsgclctun  29710  bnj1154  30321  br8  30899  br6  30900  br4  30901  fvtransport  31309  brcgr3  31323  brfs  31356  fscgr  31357  btwnconn1lem11  31374  brsegle  31385  fvray  31418  linedegen  31420  fvline  31421  poimirlem28  32607  poimirlem32  32611  heiborlem2  32781  hlsuprexch  33685  3dim1lem5  33770  lplni2  33841  2llnjN  33871  lvoli2  33885  2lplnj  33924  cdleme18d  34600  cdlemg1cex  34894  ismrc  36282  monotoddzzfi  36525  oddcomabszz  36527  zindbi  36529  rmydioph  36599  fsumiunss  38642  sumnnodd  38697  stoweidlem31  38924  stoweidlem34  38927  stoweidlem43  38936  stoweidlem48  38941  fourierdlem42  39042  sge0iunmptlemre  39308  sge0iunmpt  39311  vonioo  39573  vonicc  39576  clwwlks  41187  clwlkclwwlk  41211  clwlksfclwwlk  41269  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  av-numclwwlk5  41542