Theorem 3anbi23d 1402

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  f1dom3el3dif  6526  wrecseq123  7408  oeeui  7682  fpwwe2lem5  9456  pwfseqlem4a  9483  pwfseqlem4  9484  swrdccatin12lem3  13490  prodeq2w  14642  prodeq2ii  14643  divalg  15126  dfgcd2  15263  iscatd2  16342  posi  16950  issubg3  17612  pmtrfrn  17878  psgnunilem2  17915  psgnunilem3  17916  lmhmpropd  19073  lbsacsbs  19156  frlmphl  20120  neiptoptop  20935  neiptopnei  20936  cnhaus  21158  nrmsep  21161  dishaus  21186  ordthauslem  21187  nconnsubb  21226  pthaus  21441  txhaus  21450  xkohaus  21456  regr1lem  21542  isust  22007  ustuqtop4  22048  methaus  22325  metnrmlem3  22664  iscau4  23077  pmltpclem1  23217  dvfsumlem2  23790  aannenlem1  24083  aannenlem2  24084  istrkgcb  25355  hlbtwn  25506  iscgra  25701  dfcgra2  25721  f1otrge  25752  axlowdim  25841  axeuclidlem  25842  eengtrkg  25865  clwwlks  26879  clwlksfclwwlk  26962  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  numclwwlk5  27246  ex-opab  27289  l2p  27331  vciOLD  27416  isvclem  27432  isnvlem  27465  dipass  27700  adj1  28792  adjeq  28794  cnlnssadj  28939  br8d  29422  carsgmon  30376  carsgsigalem  30377  carsgclctunlem2  30381  carsgclctun  30383  bnj1154  31067  br8  31646  br6  31647  br4  31648  brsslt  31900  fvtransport  32139  brcgr3  32153  brfs  32186  fscgr  32187  btwnconn1lem11  32204  brsegle  32215  fvray  32248  linedegen  32250  fvline  32251  poimirlem28  33437  poimirlem32  33441  heiborlem2  33611  hlsuprexch  34667  3dim1lem5  34752  lplni2  34823  2llnjN  34853  lvoli2  34867  2lplnj  34906  cdleme18d  35582  cdlemg1cex  35876  ismrc  37264  monotoddzzfi  37507  oddcomabszz  37509  zindbi  37511  rmydioph  37581  fsumiunss  39807  sumnnodd  39862  stoweidlem31  40248  stoweidlem34  40251  stoweidlem43  40260  stoweidlem48  40265  fourierdlem42  40366  sge0iunmptlemre  40632  sge0iunmpt  40635  vonioo  40896  vonicc  40899