Theorem 3anbi23d 1440

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

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

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 398  df-3an 1090

This theorem is referenced by:  f1dom3el3dif  7268  xpord2lem  8128  xpord3lem  8135  frecseq123  8267  wrecseq123OLD  8300  oeeui  8602  sbthfi  9202  fpwwe2lem4  10629  pwfseqlem4a  10656  pwfseqlem4  10657  pfxccatin12lem3  14682  prodeq2w  15856  prodeq2ii  15857  divalg  16346  dfgcd2  16488  iscatd2  17625  posi  18270  issubg3  19024  pmtrfrn  19326  psgnunilem2  19363  psgnunilem3  19364  lmhmpropd  20684  lbsacsbs  20769  frlmphl  21336  neiptoptop  22635  neiptopnei  22636  cnhaus  22858  nrmsep  22861  dishaus  22886  ordthauslem  22887  nconnsubb  22927  pthaus  23142  txhaus  23151  xkohaus  23157  regr1lem  23243  isust  23708  ustuqtop4  23749  methaus  24029  metnrmlem3  24377  iscau4  24796  pmltpclem1  24965  dvfsumlem2  25544  aannenlem1  25841  aannenlem2  25842  brsslt  27287  istrkgcb  27707  hlbtwn  27862  iscgra  28060  dfcgra2  28081  f1otrge  28123  axlowdim  28219  axeuclidlem  28220  eengtrkg  28244  clwwlk  29236  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  numclwwlk5  29641  ex-opab  29685  l2p  29732  vciOLD  29814  isvclem  29830  isnvlem  29863  dipass  30098  adj1  31186  adjeq  31188  cnlnssadj  31333  br8d  31839  carsgmon  33313  carsgsigalem  33314  carsgclctunlem2  33318  carsgclctun  33320  bnj1154  34010  br8  34726  br6  34727  br4  34728  fvtransport  35004  brcgr3  35018  brfs  35051  fscgr  35052  btwnconn1lem11  35069  brsegle  35080  fvray  35113  linedegen  35115  fvline  35116  gg-dvfsumlem2  35183  bj-isclm  36172  poimirlem28  36516  poimirlem32  36520  heiborlem2  36680  hlsuprexch  38252  3dim1lem5  38337  lplni2  38408  2llnjN  38438  lvoli2  38452  2lplnj  38491  cdleme18d  39166  cdlemg1cex  39459  ismrc  41439  monotoddzzfi  41681  oddcomabszz  41683  zindbi  41685  rmydioph  41753  nnoeomeqom  42062  rp-brsslt  42174  fsumiunss  44291  sumnnodd  44346  stoweidlem31  44747  stoweidlem34  44750  stoweidlem43  44759  stoweidlem48  44764  fourierdlem42  44865  sge0iunmptlemre  45131  sge0iunmpt  45134  vonioo  45398  vonicc  45401  fundcmpsurinjpreimafv  46076  sepfsepc  47560  iscnrm3rlem8  47580  iscnrm3llem2  47583