Theorem 3anbi13d 1440

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 262	. 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:  3anbi3d  1444  ax12wdemo  2136  f1dom3el3dif  7244  xpord2lem  8121  xpord3lem  8128  frrlem1  8265  frrlem13  8277  cofsmo  10222  axdc3lem3  10405  axdc3lem4  10406  iscatd2  17642  psgnunilem1  19423  nn0gsumfz  19914  opprsubrg  20502  lsspropd  20924  mdetunilem3  22501  mdetunilem9  22507  smadiadetr  22562  lmres  23187  cnhaus  23241  regsep2  23263  dishaus  23269  ordthauslem  23270  nconnsubb  23310  pthaus  23525  txhaus  23534  xkohaus  23540  regr1lem  23626  ustval  24090  methaus  24408  metnrmlem3  24750  pmltpclem1  25349  brsslt  27697  axtgeucl  28399  iscgrad  28738  dfcgra2  28757  f1otrge  28799  axeuclidlem  28889  umgrvad2edg  29140  elwspths2spth  29897  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  vdgn1frgrv2  30225  numclwlk1lem1  30298  ex-opab  30361  isnvlem  30539  ajval  30790  adjeu  31818  adjval  31819  adj1  31862  adjeq  31864  cnlnssadj  32009  br8d  32538  lt2addrd  32674  xlt2addrd  32682  crngmxidl  33440  constrconj  33735  constrllcllem  33742  constrcccllem  33744  constrcbvlem  33745  measval  34188  loop1cycl  35124  br8  35743  br6  35744  br4  35745  brcgr3  36034  brsegle  36096  fvray  36129  linedegen  36131  fvline  36132  poimirlem28  37642  isopos  39173  hlsuprexch  39375  2llnjN  39561  2lplnj  39614  cdlemk42  40935  zindbi  42935  jm2.27  42997  nnoeomeqom  43301  tfsconcatrev  43337  rp-brsslt  43412  stoweidlem43  46041  fourierdlem42  46147  ichexmpl1  47470  vopnbgrel  47854  dfclnbgr6  47856  dfnbgr6  47857  cycl3grtri  47946  grimgrtri  47948  usgrgrtrirex  47949  grlimgrtri  47995  usgrexmpl1tri  48016  sepfsepc  48916  iscnrm3rlem8  48935  iscnrm3llem2  48938