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  2140  f1dom3el3dif  7215  xpord2lem  8084  xpord3lem  8091  frrlem1  8228  frrlem13  8240  cofsmo  10179  axdc3lem3  10362  axdc3lem4  10363  iscatd2  17604  psgnunilem1  19422  nn0gsumfz  19913  opprsubrg  20526  lsspropd  20969  mdetunilem3  22558  mdetunilem9  22564  smadiadetr  22619  lmres  23244  cnhaus  23298  regsep2  23320  dishaus  23326  ordthauslem  23327  nconnsubb  23367  pthaus  23582  txhaus  23591  xkohaus  23597  regr1lem  23683  ustval  24147  methaus  24464  metnrmlem3  24806  pmltpclem1  25405  brslts  27758  bdayfinbndcbv  28462  bdayfinbndlem1  28463  bdayfinbndlem2  28464  axtgeucl  28544  iscgrad  28883  dfcgra2  28902  f1otrge  28944  axeuclidlem  29035  umgrvad2edg  29286  elwspths2spth  30043  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  vdgn1frgrv2  30371  numclwlk1lem1  30444  ex-opab  30507  isnvlem  30685  ajval  30936  adjeu  31964  adjval  31965  adj1  32008  adjeq  32010  cnlnssadj  32155  br8d  32686  lt2addrd  32830  xlt2addrd  32839  crngmxidl  33550  constrconj  33902  constrllcllem  33909  constrcccllem  33911  constrcbvlem  33912  measval  34355  tz9.1regs  35290  loop1cycl  35331  br8  35950  br6  35951  br4  35952  brcgr3  36240  brsegle  36302  fvray  36335  linedegen  36337  fvline  36338  poimirlem28  37849  isopos  39440  hlsuprexch  39641  2llnjN  39827  2lplnj  39880  cdlemk42  41201  zindbi  43188  jm2.27  43250  nnoeomeqom  43554  tfsconcatrev  43590  rp-brsslt  43664  stoweidlem43  46287  fourierdlem42  46393  ichexmpl1  47715  vopnbgrel  48100  dfclnbgr6  48102  dfnbgr6  48103  cycl3grtri  48193  grimgrtri  48195  usgrgrtrirex  48196  grlimgrtri  48249  usgrexmpl1tri  48271  sepfsepc  49173  iscnrm3rlem8  49192  iscnrm3llem2  49195