Theorem 3anbi23d 1461

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 1458	1 ⊢ (𝜑 → ((𝜂 ∧ 𝜓 ∧ 𝜃) ↔ (𝜂 ∧ 𝜒 ∧ 𝜏)))

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

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 400  df-3an 1101

This theorem is referenced by:  f1dom3el3dif  7254  xpord2lem  8123  xpord3lem  8130  frecseq123  8264  oeeui  8573  sbthfi  9168  pwfseqlem4a  10620  pwfseqlem4  10621  pfxccatin12lem3  14746  prodeq2w  15941  prodeq2ii  15942  prodeq2sdv  15954  divalg  16438  dfgcd2  16581  iscatd2  17714  posi  18350  issubg3  19187  pmtrfrn  19499  psgnunilem2  19536  psgnunilem3  19537  lmhmpropd  21141  lbsacsbs  21227  frlmphl  21834  neiptoptop  23192  neiptopnei  23193  cnhaus  23415  nrmsep  23418  dishaus  23443  ordthauslem  23444  nconnsubb  23484  pthaus  23699  txhaus  23708  xkohaus  23714  regr1lem  23800  isust  24265  ustuqtop4  24305  methaus  24581  metnrmlem3  24923  iscau4  25342  pmltpclem1  25511  dvfsumlem2  26090  aannenlem1  26393  aannenlem2  26394  brslts  27856  bdayfinbndlem1  28561  istrkgcb  28626  hlbtwn  28781  iscgra  29004  dfcgra2  29025  f1otrge  29073  axlowdim  29163  axeuclidlem  29164  eengtrkg  29188  clwwlk  30186  upgr3v3e3cycl  30383  upgr4cycl4dv4e  30388  numclwwlk5  30591  ex-opab  30635  l2p  30683  vciOLD  30765  isvclem  30781  isnvlem  30814  dipass  31049  adj1  32137  adjeq  32139  cnlnssadj  32284  br8d  32811  dvdsruasso2  33573  dfufd2lem  33746  constrsuc  34036  constrconj  34043  constrllcllem  34050  constrcbvlem  34053  carsgmon  34612  carsgsigalem  34613  carsgclctunlem2  34617  carsgclctun  34619  bnj1154  35295  br8  36107  br6  36108  br4  36109  fvtransport  36383  brcgr3  36397  brfs  36430  fscgr  36431  btwnconn1lem11  36448  brsegle  36459  fvray  36492  linedegen  36494  fvline  36495  cbvproddavw  36641  bj-isclm  37784  poimirlem28  38148  poimirlem32  38152  heiborlem2  38312  hlsuprexch  40006  3dim1lem5  40091  lplni2  40162  2llnjN  40192  lvoli2  40206  2lplnj  40245  cdleme18d  40920  cdlemg1cex  41213  ismrc  43283  monotoddzzfi  43520  oddcomabszz  43522  zindbi  43524  rmydioph  43592  nnoeomeqom  43890  rp-brsslt  44000  fsumiunss  46152  sumnnodd  46207  stoweidlem31  46606  stoweidlem34  46609  stoweidlem43  46618  stoweidlem48  46623  fourierdlem42  46724  sge0iunmptlemre  46990  sge0iunmpt  46993  vonioo  47257  vonicc  47260  fundcmpsurinjpreimafv  48015  upgrimpths  48532  cycl3grtri  48570  grimgrtri  48572  usgrgrtrirex  48573  grlimgrtri  48626  sepfsepc  49550  iscnrm3rlem8  49569  iscnrm3llem2  49572