Theorem 3anbi23d 1467

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  f1dom3el3dif  7283  xpord2lem  8172  xpord3lem  8179  frecseq123  8314  oeeui  8625  sbthfi  9228  pwfseqlem4a  10759  pwfseqlem4  10760  pfxccatin12lem3  14895  prodeq2w  16094  prodeq2ii  16095  prodeq2sdv  16106  divalg  16588  dfgcd2  16734  iscatd2  17870  posi  18506  issubg3  19370  pmtrfrn  19687  psgnunilem2  19724  psgnunilem3  19725  lmhmpropd  21363  lbsacsbs  21449  frlmphl  22102  neiptoptop  23464  neiptopnei  23465  cnhaus  23687  nrmsep  23690  dishaus  23715  ordthauslem  23716  nconnsubb  23756  pthaus  23972  txhaus  23981  xkohaus  23987  regr1lem  24073  isust  24538  ustuqtop4  24578  methaus  24854  metnrmlem3  25196  iscau4  25615  pmltpclem1  25784  dvfsumlem2  26362  aannenlem1  26670  aannenlem2  26671  brslts  28163  bdayfinbndlem1  28868  istrkgcb  28933  hlbtwn  29092  iscgra  29331  dfcgra2  29353  f1otrge  29464  axlowdim  29554  axeuclidlem  29555  eengtrkg  29579  clwwlk  30589  upgr3v3e3cycl  30796  upgr4cycl4dv4e  30801  numclwwlk5  31004  ex-opab  31048  l2p  31096  vciOLD  31178  isvclem  31194  isnvlem  31227  dipass  31462  adj1  32550  adjeq  32552  cnlnssadj  32697  br8d  33259  dvdsruasso2  33997  dfufd2lem  34137  constrsuc  34426  constrconj  34433  constrllcllem  34440  constrcbvlem  34443  carsgmon  35002  carsgsigalem  35003  carsgclctunlem2  35007  carsgclctun  35009  bnj1154  35685  onprcf1acwevdlem1  36002  br8  36651  br6  36652  br4  36653  fvtransport  36927  brcgr3  36941  brfs  36974  fscgr  36975  btwnconn1lem11  36992  brsegle  37003  fvray  37036  linedegen  37038  fvline  37039  cbvproddavw  37199  bj-isclm  38355  poimirlem28  38709  poimirlem32  38713  heiborlem2  38889  hlsuprexch  40581  3dim1lem5  40666  lplni2  40737  2llnjN  40767  lvoli2  40781  2lplnj  40820  cdleme18d  41495  cdlemg1cex  41788  ismrc  43855  monotoddzzfi  44092  oddcomabszz  44094  zindbi  44096  rmydioph  44164  nnoeomeqom  44457  rp-brsslt  44567  fsumiunss  46729  sumnnodd  46784  stoweidlem31  47183  stoweidlem34  47186  stoweidlem43  47195  stoweidlem48  47200  fourierdlem42  47301  sge0iunmptlemre  47567  sge0iunmpt  47570  vonioo  47834  vonicc  47837  fundcmpsurinjpreimafv  48632  upgrimpths  49149  cycl3grtri  49187  grimgrtri  49189  usgrgrtrirex  49190  grlimgrtri  49243  sepfsepc  50184  iscnrm3rlem8  50203  iscnrm3llem2  50206