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  7206  xpord2lem  8075  xpord3lem  8082  frecseq123  8215  oeeui  8520  sbthfi  9113  pwfseqlem4a  10555  pwfseqlem4  10556  pfxccatin12lem3  14638  prodeq2w  15817  prodeq2ii  15818  prodeq2sdv  15830  divalg  16314  dfgcd2  16457  iscatd2  17587  posi  18223  issubg3  19023  pmtrfrn  19337  psgnunilem2  19374  psgnunilem3  19375  lmhmpropd  20977  lbsacsbs  21063  frlmphl  21688  neiptoptop  23016  neiptopnei  23017  cnhaus  23239  nrmsep  23242  dishaus  23267  ordthauslem  23268  nconnsubb  23308  pthaus  23523  txhaus  23532  xkohaus  23538  regr1lem  23624  isust  24089  ustuqtop4  24130  methaus  24406  metnrmlem3  24748  iscau4  25177  pmltpclem1  25347  dvfsumlem2  25931  dvfsumlem2OLD  25932  aannenlem1  26234  aannenlem2  26235  brsslt  27696  istrkgcb  28401  hlbtwn  28556  iscgra  28754  dfcgra2  28775  f1otrge  28817  axlowdim  28906  axeuclidlem  28907  eengtrkg  28931  clwwlk  29927  upgr3v3e3cycl  30124  upgr4cycl4dv4e  30129  numclwwlk5  30332  ex-opab  30376  l2p  30423  vciOLD  30505  isvclem  30521  isnvlem  30554  dipass  30789  adj1  31877  adjeq  31879  cnlnssadj  32024  br8d  32555  dvdsruasso2  33324  dfufd2lem  33487  constrsuc  33711  constrconj  33718  constrllcllem  33725  constrcbvlem  33728  carsgmon  34288  carsgsigalem  34289  carsgclctunlem2  34293  carsgclctun  34295  bnj1154  34972  br8  35739  br6  35740  br4  35741  fvtransport  36016  brcgr3  36030  brfs  36063  fscgr  36064  btwnconn1lem11  36081  brsegle  36092  fvray  36125  linedegen  36127  fvline  36128  cbvproddavw  36264  bj-isclm  37275  poimirlem28  37638  poimirlem32  37642  heiborlem2  37802  hlsuprexch  39370  3dim1lem5  39455  lplni2  39526  2llnjN  39556  lvoli2  39570  2lplnj  39609  cdleme18d  40284  cdlemg1cex  40577  ismrc  42684  monotoddzzfi  42925  oddcomabszz  42927  zindbi  42929  rmydioph  42997  nnoeomeqom  43295  rp-brsslt  43406  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  47903  cycl3grtri  47941  grimgrtri  47943  usgrgrtrirex  47944  grlimgrtri  47997  sepfsepc  48922  iscnrm3rlem8  48941  iscnrm3llem2  48944