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

Proof of Theorem 3anbi13d

Step	Hyp	Ref	Expression
1		3anbi12d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		biidd 265	. 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂))
3		3anbi12d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	1, 2, 3	3anbi123d 1465	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:  3anbi3d  1471  ax12wdemo  2174  f1dom3el3dif  7304  xpord2lem  8196  xpord3lem  8203  frrlem1  8342  frrlem13  8354  cofsmo  10386  axdc3lem3  10569  axdc3lem4  10570  iscatd2  17905  psgnunilem1  19758  nn0gsumfz  20249  opprsubrg  20896  lsspropd  21343  mdetunilem3  22984  mdetunilem9  22990  smadiadetr  23045  lmres  23673  cnhaus  23727  regsep2  23749  dishaus  23755  ordthauslem  23756  nconnsubb  23796  pthaus  24012  txhaus  24021  xkohaus  24027  regr1lem  24113  ustval  24577  methaus  24894  metnrmlem3  25236  pmltpclem1  25824  brslts  28205  bdayfinbndcbv  28909  bdayfinbndlem1  28910  bdayfinbndlem2  28911  axtgeucl  28991  iscgrad  29375  dfcgra2  29395  f1otrge  29506  axeuclidlem  29597  umgrvad2edg  29851  elwspths2spth  30616  loop1cycl  30801  upgr3v3e3cycl  30838  upgr4cycl4dv4e  30843  vdgn1frgrv2  30954  numclwlk1lem1  31027  ex-opab  31090  isnvlem  31269  ajval  31520  adjeu  32548  adjval  32549  adj1  32592  adjeq  32594  cnlnssadj  32739  br8d  33300  lt2addrd  33438  xlt2addrd  33447  crngmxidl  34098  constrconj  34488  constrllcllem  34495  constrcccllem  34497  constrcbvlem  34498  measval  34942  tz9.1regs  35943  br8  36736  br6  36737  br4  36738  brcgr3  37026  brsegle  37088  fvray  37121  linedegen  37123  fvline  37124  poimirlem28  38834  isopos  40503  hlsuprexch  40704  2llnjN  40890  2lplnj  40943  cdlemk42  42264  zindbi  44219  jm2.27  44281  nnoeomeqom  44575  tfsconcatrev  44611  rp-brsslt  44685  stoweidlem43  47326  fourierdlem42  47432  ichexmpl1  48824  vopnbgrel  49225  dfclnbgr6  49227  dfnbgr6  49228  cycl3grtri  49318  grimgrtri  49320  usgrgrtrirex  49321  grlimgrtri  49374  usgrexmpl1tri  49396  sepfsepc  50373  iscnrm3rlem8  50392  iscnrm3llem2  50395