Theorem 3anbi23d 1441

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1089

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

This theorem is referenced by:  f1dom3el3dif  7059  frecseq123  8002  wrecseq123  8026  oeeui  8308  fpwwe2lem4  10213  pwfseqlem4a  10240  pwfseqlem4  10241  pfxccatin12lem3  14262  prodeq2w  15437  prodeq2ii  15438  divalg  15927  dfgcd2  16069  iscatd2  17138  posi  17778  issubg3  18515  pmtrfrn  18804  psgnunilem2  18841  psgnunilem3  18842  lmhmpropd  20064  lbsacsbs  20147  frlmphl  20697  neiptoptop  21982  neiptopnei  21983  cnhaus  22205  nrmsep  22208  dishaus  22233  ordthauslem  22234  nconnsubb  22274  pthaus  22489  txhaus  22498  xkohaus  22504  regr1lem  22590  isust  23055  ustuqtop4  23096  methaus  23372  metnrmlem3  23712  iscau4  24130  pmltpclem1  24299  dvfsumlem2  24878  aannenlem1  25175  aannenlem2  25176  istrkgcb  26501  hlbtwn  26656  iscgra  26854  dfcgra2  26875  f1otrge  26917  axlowdim  27006  axeuclidlem  27007  eengtrkg  27031  clwwlk  28020  upgr3v3e3cycl  28217  upgr4cycl4dv4e  28222  numclwwlk5  28425  ex-opab  28469  l2p  28514  vciOLD  28596  isvclem  28612  isnvlem  28645  dipass  28880  adj1  29968  adjeq  29970  cnlnssadj  30115  br8d  30623  carsgmon  31947  carsgsigalem  31948  carsgclctunlem2  31952  carsgclctun  31954  bnj1154  32646  br8  33393  br6  33394  br4  33395  xpord2lem  33469  xpord3lem  33475  brsslt  33666  fvtransport  34020  brcgr3  34034  brfs  34067  fscgr  34068  btwnconn1lem11  34085  brsegle  34096  fvray  34129  linedegen  34131  fvline  34132  bj-isclm  35145  poimirlem28  35491  poimirlem32  35495  heiborlem2  35656  hlsuprexch  37081  3dim1lem5  37166  lplni2  37237  2llnjN  37267  lvoli2  37281  2lplnj  37320  cdleme18d  37995  cdlemg1cex  38288  ismrc  40167  monotoddzzfi  40408  oddcomabszz  40410  zindbi  40412  rmydioph  40480  fsumiunss  42734  sumnnodd  42789  stoweidlem31  43190  stoweidlem34  43193  stoweidlem43  43202  stoweidlem48  43207  fourierdlem42  43308  sge0iunmptlemre  43571  sge0iunmpt  43574  vonioo  43838  vonicc  43841  fundcmpsurinjpreimafv  44476  sepfsepc  45837  iscnrm3rlem8  45857  iscnrm3llem2  45860