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

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

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 1088

This theorem is referenced by:  f1dom3el3dif  7226  xpord2lem  8098  xpord3lem  8105  frecseq123  8238  oeeui  8543  sbthfi  9140  pwfseqlem4a  10590  pwfseqlem4  10591  pfxccatin12lem3  14673  prodeq2w  15852  prodeq2ii  15853  prodeq2sdv  15865  divalg  16349  dfgcd2  16492  iscatd2  17622  posi  18258  issubg3  19058  pmtrfrn  19372  psgnunilem2  19409  psgnunilem3  19410  lmhmpropd  21012  lbsacsbs  21098  frlmphl  21723  neiptoptop  23051  neiptopnei  23052  cnhaus  23274  nrmsep  23277  dishaus  23302  ordthauslem  23303  nconnsubb  23343  pthaus  23558  txhaus  23567  xkohaus  23573  regr1lem  23659  isust  24124  ustuqtop4  24165  methaus  24441  metnrmlem3  24783  iscau4  25212  pmltpclem1  25382  dvfsumlem2  25966  dvfsumlem2OLD  25967  aannenlem1  26269  aannenlem2  26270  brsslt  27731  istrkgcb  28436  hlbtwn  28591  iscgra  28789  dfcgra2  28810  f1otrge  28852  axlowdim  28941  axeuclidlem  28942  eengtrkg  28966  clwwlk  29962  upgr3v3e3cycl  30159  upgr4cycl4dv4e  30164  numclwwlk5  30367  ex-opab  30411  l2p  30458  vciOLD  30540  isvclem  30556  isnvlem  30589  dipass  30824  adj1  31912  adjeq  31914  cnlnssadj  32059  br8d  32588  dvdsruasso2  33350  dfufd2lem  33513  constrsuc  33721  constrconj  33728  constrllcllem  33735  constrcbvlem  33738  carsgmon  34298  carsgsigalem  34299  carsgclctunlem2  34303  carsgclctun  34305  bnj1154  34982  br8  35736  br6  35737  br4  35738  fvtransport  36013  brcgr3  36027  brfs  36060  fscgr  36061  btwnconn1lem11  36078  brsegle  36089  fvray  36122  linedegen  36124  fvline  36125  cbvproddavw  36261  bj-isclm  37272  poimirlem28  37635  poimirlem32  37639  heiborlem2  37799  hlsuprexch  39368  3dim1lem5  39453  lplni2  39524  2llnjN  39554  lvoli2  39568  2lplnj  39607  cdleme18d  40282  cdlemg1cex  40575  ismrc  42682  monotoddzzfi  42924  oddcomabszz  42926  zindbi  42928  rmydioph  42996  nnoeomeqom  43294  rp-brsslt  43405  fsumiunss  45566  sumnnodd  45621  stoweidlem31  46022  stoweidlem34  46025  stoweidlem43  46034  stoweidlem48  46039  fourierdlem42  46140  sge0iunmptlemre  46406  sge0iunmpt  46409  vonioo  46673  vonicc  46676  fundcmpsurinjpreimafv  47402  upgrimpths  47902  cycl3grtri  47939  grimgrtri  47941  usgrgrtrirex  47942  grlimgrtri  47988  sepfsepc  48909  iscnrm3rlem8  48928  iscnrm3llem2  48931