Theorem 3anbi23d 1556

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

Syntax hints:   → wi 4   ↔ wb 197   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  f1dom3el3dif  6746  wrecseq123  7639  oeeui  7915  fpwwe2lem5  9737  pwfseqlem4a  9764  pwfseqlem4  9765  swrdccatin12lem3  13710  prodeq2w  14859  prodeq2ii  14860  divalg  15342  dfgcd2  15478  iscatd2  16542  posi  17151  issubg3  17810  pmtrfrn  18075  psgnunilem2  18112  psgnunilem3  18113  lmhmpropd  19276  lbsacsbs  19361  frlmphl  20326  neiptoptop  21145  neiptopnei  21146  cnhaus  21368  nrmsep  21371  dishaus  21396  ordthauslem  21397  nconnsubb  21436  pthaus  21651  txhaus  21660  xkohaus  21666  regr1lem  21752  isust  22216  ustuqtop4  22257  methaus  22534  metnrmlem3  22873  iscau4  23285  pmltpclem1  23425  dvfsumlem2  24000  aannenlem1  24293  aannenlem2  24294  istrkgcb  25565  hlbtwn  25716  iscgra  25911  dfcgra2  25931  f1otrge  25962  axlowdim  26051  axeuclidlem  26052  eengtrkg  26075  clwwlk  27122  clwlksfclwwlkOLD  27232  upgr3v3e3cycl  27349  upgr4cycl4dv4e  27354  numclwwlk5  27572  ex-opab  27616  l2p  27658  vciOLD  27740  isvclem  27756  isnvlem  27789  dipass  28024  adj1  29116  adjeq  29118  cnlnssadj  29263  br8d  29743  carsgmon  30697  carsgsigalem  30698  carsgclctunlem2  30702  carsgclctun  30704  bnj1154  31385  br8  31963  br6  31964  br4  31965  frecseq123  32093  brsslt  32216  fvtransport  32455  brcgr3  32469  brfs  32502  fscgr  32503  btwnconn1lem11  32520  brsegle  32531  fvray  32564  linedegen  32566  fvline  32567  poimirlem28  33745  poimirlem32  33749  heiborlem2  33917  hlsuprexch  35156  3dim1lem5  35241  lplni2  35312  2llnjN  35342  lvoli2  35356  2lplnj  35395  cdleme18d  36070  cdlemg1cex  36363  ismrc  37760  monotoddzzfi  38002  oddcomabszz  38004  zindbi  38006  rmydioph  38076  fsumiunss  40281  sumnnodd  40336  stoweidlem31  40721  stoweidlem34  40724  stoweidlem43  40733  stoweidlem48  40738  fourierdlem42  40839  sge0iunmptlemre  41105  sge0iunmpt  41108  vonioo  41372  vonicc  41375