Theorem 3anbi13d 1466

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 1464	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  1470  ax12wdemo  2172  f1dom3el3dif  7266  xpord2lem  8140  xpord3lem  8147  frrlem1  8285  frrlem13  8297  cofsmo  10271  axdc3lem3  10454  axdc3lem4  10455  iscatd2  17769  psgnunilem1  19620  nn0gsumfz  20111  opprsubrg  20755  lsspropd  21201  mdetunilem3  22836  mdetunilem9  22842  smadiadetr  22897  lmres  23525  cnhaus  23579  regsep2  23601  dishaus  23607  ordthauslem  23608  nconnsubb  23648  pthaus  23864  txhaus  23873  xkohaus  23879  regr1lem  23965  ustval  24429  methaus  24746  metnrmlem3  25088  pmltpclem1  25676  brslts  28027  bdayfinbndcbv  28731  bdayfinbndlem1  28732  bdayfinbndlem2  28733  axtgeucl  28813  iscgrad  29197  dfcgra2  29217  f1otrge  29328  axeuclidlem  29419  umgrvad2edg  29673  elwspths2spth  30438  loop1cycl  30623  upgr3v3e3cycl  30660  upgr4cycl4dv4e  30665  vdgn1frgrv2  30776  numclwlk1lem1  30849  ex-opab  30912  isnvlem  31091  ajval  31342  adjeu  32370  adjval  32371  adj1  32414  adjeq  32416  cnlnssadj  32561  br8d  33081  lt2addrd  33221  xlt2addrd  33230  crngmxidl  33872  constrconj  34255  constrllcllem  34262  constrcccllem  34264  constrcbvlem  34265  measval  34709  tz9.1regs  35660  br8  36335  br6  36336  br4  36337  brcgr3  36626  brsegle  36688  fvray  36721  linedegen  36723  fvline  36724  poimirlem28  38397  isopos  40053  hlsuprexch  40254  2llnjN  40440  2lplnj  40493  cdlemk42  41814  zindbi  43787  jm2.27  43849  nnoeomeqom  44153  tfsconcatrev  44189  rp-brsslt  44263  stoweidlem43  46871  fourierdlem42  46977  ichexmpl1  48369  vopnbgrel  48770  dfclnbgr6  48772  dfnbgr6  48773  cycl3grtri  48863  grimgrtri  48865  usgrgrtrirex  48866  grlimgrtri  48919  usgrexmpl1tri  48941  sepfsepc  49854  iscnrm3rlem8  49873  iscnrm3llem2  49876