Theorem 3anbi23d 1442

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

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

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 1089

This theorem is referenced by:  f1dom3el3dif  7225  xpord2lem  8094  xpord3lem  8101  frecseq123  8234  oeeui  8540  sbthfi  9135  pwfseqlem4a  10584  pwfseqlem4  10585  pfxccatin12lem3  14667  prodeq2w  15845  prodeq2ii  15846  prodeq2sdv  15858  divalg  16342  dfgcd2  16485  iscatd2  17616  posi  18252  issubg3  19089  pmtrfrn  19402  psgnunilem2  19439  psgnunilem3  19440  lmhmpropd  21040  lbsacsbs  21126  frlmphl  21751  neiptoptop  23090  neiptopnei  23091  cnhaus  23313  nrmsep  23316  dishaus  23341  ordthauslem  23342  nconnsubb  23382  pthaus  23597  txhaus  23606  xkohaus  23612  regr1lem  23698  isust  24163  ustuqtop4  24203  methaus  24479  metnrmlem3  24821  iscau4  25250  pmltpclem1  25420  dvfsumlem2  26004  dvfsumlem2OLD  26005  aannenlem1  26307  aannenlem2  26308  brslts  27773  bdayfinbndlem1  28478  istrkgcb  28543  hlbtwn  28699  iscgra  28897  dfcgra2  28918  f1otrge  28960  axlowdim  29050  axeuclidlem  29051  eengtrkg  29075  clwwlk  30074  upgr3v3e3cycl  30271  upgr4cycl4dv4e  30276  numclwwlk5  30479  ex-opab  30523  l2p  30571  vciOLD  30653  isvclem  30669  isnvlem  30702  dipass  30937  adj1  32025  adjeq  32027  cnlnssadj  32172  br8d  32702  dvdsruasso2  33483  dfufd2lem  33646  constrsuc  33920  constrconj  33927  constrllcllem  33934  constrcbvlem  33937  carsgmon  34496  carsgsigalem  34497  carsgclctunlem2  34501  carsgclctun  34503  bnj1154  35179  br8  35976  br6  35977  br4  35978  fvtransport  36252  brcgr3  36266  brfs  36299  fscgr  36300  btwnconn1lem11  36317  brsegle  36328  fvray  36361  linedegen  36363  fvline  36364  cbvproddavw  36500  bj-isclm  37550  poimirlem28  37903  poimirlem32  37907  heiborlem2  38067  hlsuprexch  39761  3dim1lem5  39846  lplni2  39917  2llnjN  39947  lvoli2  39961  2lplnj  40000  cdleme18d  40675  cdlemg1cex  40968  ismrc  43062  monotoddzzfi  43303  oddcomabszz  43305  zindbi  43307  rmydioph  43375  nnoeomeqom  43673  rp-brsslt  43783  fsumiunss  45939  sumnnodd  45994  stoweidlem31  46393  stoweidlem34  46396  stoweidlem43  46405  stoweidlem48  46410  fourierdlem42  46511  sge0iunmptlemre  46777  sge0iunmpt  46780  vonioo  47044  vonicc  47047  fundcmpsurinjpreimafv  47772  upgrimpths  48273  cycl3grtri  48311  grimgrtri  48313  usgrgrtrirex  48314  grlimgrtri  48367  sepfsepc  49291  iscnrm3rlem8  49310  iscnrm3llem2  49313