Theorem 3anbi13d 1446

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 263	. 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂))
3		3anbi12d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	1, 2, 3	3anbi123d 1444	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜂 ∧ 𝜃) ↔ (𝜒 ∧ 𝜂 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3anbi3d  1450  ax12wdemo  2146  f1dom3el3dif  7213  xpord2lem  8082  xpord3lem  8089  frrlem1  8226  frrlem13  8238  cofsmo  10182  axdc3lem3  10365  axdc3lem4  10366  iscatd2  17638  psgnunilem1  19459  nn0gsumfz  19950  opprsubrg  20565  lsspropd  21007  mdetunilem3  22597  mdetunilem9  22603  smadiadetr  22658  lmres  23283  cnhaus  23337  regsep2  23359  dishaus  23365  ordthauslem  23366  nconnsubb  23406  pthaus  23621  txhaus  23630  xkohaus  23636  regr1lem  23722  ustval  24186  methaus  24503  metnrmlem3  24845  pmltpclem1  25433  brslts  27772  bdayfinbndcbv  28476  bdayfinbndlem1  28477  bdayfinbndlem2  28478  axtgeucl  28558  iscgrad  28897  dfcgra2  28916  f1otrge  28958  axeuclidlem  29049  umgrvad2edg  29300  elwspths2spth  30056  upgr3v3e3cycl  30268  upgr4cycl4dv4e  30273  vdgn1frgrv2  30384  numclwlk1lem1  30457  ex-opab  30520  isnvlem  30699  ajval  30950  adjeu  31978  adjval  31979  adj1  32022  adjeq  32024  cnlnssadj  32169  br8d  32700  lt2addrd  32842  xlt2addrd  32851  crngmxidl  33552  constrconj  33929  constrllcllem  33936  constrcccllem  33938  constrcbvlem  33939  measval  34382  tz9.1regs  35315  loop1cycl  35365  br8  35984  br6  35985  br4  35986  brcgr3  36274  brsegle  36336  fvray  36369  linedegen  36371  fvline  36372  poimirlem28  38015  isopos  39672  hlsuprexch  39873  2llnjN  40059  2lplnj  40112  cdlemk42  41433  zindbi  43391  jm2.27  43453  nnoeomeqom  43757  tfsconcatrev  43793  rp-brsslt  43867  stoweidlem43  46486  fourierdlem42  46592  ichexmpl1  47944  vopnbgrel  48345  dfclnbgr6  48347  dfnbgr6  48348  cycl3grtri  48438  grimgrtri  48440  usgrgrtrirex  48441  grlimgrtri  48494  usgrexmpl1tri  48516  sepfsepc  49418  iscnrm3rlem8  49437  iscnrm3llem2  49440