Theorem 3anbi23d 1437

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  f1dom3el3dif  7136  frecseq123  8082  wrecseq123OLD  8115  oeeui  8409  sbthfi  8950  fpwwe2lem4  10374  pwfseqlem4a  10401  pwfseqlem4  10402  pfxccatin12lem3  14426  prodeq2w  15603  prodeq2ii  15604  divalg  16093  dfgcd2  16235  iscatd2  17371  posi  18016  issubg3  18754  pmtrfrn  19047  psgnunilem2  19084  psgnunilem3  19085  lmhmpropd  20316  lbsacsbs  20399  frlmphl  20969  neiptoptop  22263  neiptopnei  22264  cnhaus  22486  nrmsep  22489  dishaus  22514  ordthauslem  22515  nconnsubb  22555  pthaus  22770  txhaus  22779  xkohaus  22785  regr1lem  22871  isust  23336  ustuqtop4  23377  methaus  23657  metnrmlem3  24005  iscau4  24424  pmltpclem1  24593  dvfsumlem2  25172  aannenlem1  25469  aannenlem2  25470  istrkgcb  26798  hlbtwn  26953  iscgra  27151  dfcgra2  27172  f1otrge  27214  axlowdim  27310  axeuclidlem  27311  eengtrkg  27335  clwwlk  28326  upgr3v3e3cycl  28523  upgr4cycl4dv4e  28528  numclwwlk5  28731  ex-opab  28775  l2p  28820  vciOLD  28902  isvclem  28918  isnvlem  28951  dipass  29186  adj1  30274  adjeq  30276  cnlnssadj  30421  br8d  30929  carsgmon  32260  carsgsigalem  32261  carsgclctunlem2  32265  carsgclctun  32267  bnj1154  32958  br8  33702  br6  33703  br4  33704  xpord2lem  33768  xpord3lem  33774  brsslt  33959  fvtransport  34313  brcgr3  34327  brfs  34360  fscgr  34361  btwnconn1lem11  34378  brsegle  34389  fvray  34422  linedegen  34424  fvline  34425  bj-isclm  35441  poimirlem28  35784  poimirlem32  35788  heiborlem2  35949  hlsuprexch  37374  3dim1lem5  37459  lplni2  37530  2llnjN  37560  lvoli2  37574  2lplnj  37613  cdleme18d  38288  cdlemg1cex  38581  ismrc  40503  monotoddzzfi  40744  oddcomabszz  40746  zindbi  40748  rmydioph  40816  fsumiunss  43070  sumnnodd  43125  stoweidlem31  43526  stoweidlem34  43529  stoweidlem43  43538  stoweidlem48  43543  fourierdlem42  43644  sge0iunmptlemre  43907  sge0iunmpt  43910  vonioo  44174  vonicc  44177  fundcmpsurinjpreimafv  44812  sepfsepc  46173  iscnrm3rlem8  46193  iscnrm3llem2  46196