Theorem 3anbi23d 1442

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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 1089

This theorem is referenced by:  f1dom3el3dif  7224  xpord2lem  8092  xpord3lem  8099  frecseq123  8232  oeeui  8538  sbthfi  9133  pwfseqlem4a  10584  pwfseqlem4  10585  pfxccatin12lem3  14694  prodeq2w  15875  prodeq2ii  15876  prodeq2sdv  15888  divalg  16372  dfgcd2  16515  iscatd2  17647  posi  18283  issubg3  19120  pmtrfrn  19433  psgnunilem2  19470  psgnunilem3  19471  lmhmpropd  21068  lbsacsbs  21154  frlmphl  21761  neiptoptop  23096  neiptopnei  23097  cnhaus  23319  nrmsep  23322  dishaus  23347  ordthauslem  23348  nconnsubb  23388  pthaus  23603  txhaus  23612  xkohaus  23618  regr1lem  23704  isust  24169  ustuqtop4  24209  methaus  24485  metnrmlem3  24827  iscau4  25246  pmltpclem1  25415  dvfsumlem2  25994  aannenlem1  26294  aannenlem2  26295  brslts  27754  bdayfinbndlem1  28459  istrkgcb  28524  hlbtwn  28679  iscgra  28877  dfcgra2  28898  f1otrge  28940  axlowdim  29030  axeuclidlem  29031  eengtrkg  29055  clwwlk  30053  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  numclwwlk5  30458  ex-opab  30502  l2p  30550  vciOLD  30632  isvclem  30648  isnvlem  30681  dipass  30916  adj1  32004  adjeq  32006  cnlnssadj  32151  br8d  32681  dvdsruasso2  33446  dfufd2lem  33609  constrsuc  33882  constrconj  33889  constrllcllem  33896  constrcbvlem  33899  carsgmon  34458  carsgsigalem  34459  carsgclctunlem2  34463  carsgclctun  34465  bnj1154  35141  br8  35938  br6  35939  br4  35940  fvtransport  36214  brcgr3  36228  brfs  36261  fscgr  36262  btwnconn1lem11  36279  brsegle  36290  fvray  36323  linedegen  36325  fvline  36326  cbvproddavw  36462  bj-isclm  37605  poimirlem28  37969  poimirlem32  37973  heiborlem2  38133  hlsuprexch  39827  3dim1lem5  39912  lplni2  39983  2llnjN  40013  lvoli2  40027  2lplnj  40066  cdleme18d  40741  cdlemg1cex  41034  ismrc  43133  monotoddzzfi  43370  oddcomabszz  43372  zindbi  43374  rmydioph  43442  nnoeomeqom  43740  rp-brsslt  43850  fsumiunss  46005  sumnnodd  46060  stoweidlem31  46459  stoweidlem34  46462  stoweidlem43  46471  stoweidlem48  46476  fourierdlem42  46577  sge0iunmptlemre  46843  sge0iunmpt  46846  vonioo  47110  vonicc  47113  fundcmpsurinjpreimafv  47868  upgrimpths  48385  cycl3grtri  48423  grimgrtri  48425  usgrgrtrirex  48426  grlimgrtri  48479  sepfsepc  49403  iscnrm3rlem8  49422  iscnrm3llem2  49425