Theorem 3anbi13d 1464

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3anbi3d  1468  ax12wdemo  2176  f1dom3el3dif  7268  xpord2lem  8137  xpord3lem  8144  frrlem1  8282  frrlem13  8294  cofsmo  10252  axdc3lem3  10435  axdc3lem4  10436  iscatd2  17736  psgnunilem1  19562  nn0gsumfz  20053  opprsubrg  20677  lsspropd  21115  mdetunilem3  22739  mdetunilem9  22745  smadiadetr  22800  lmres  23425  cnhaus  23479  regsep2  23501  dishaus  23507  ordthauslem  23508  nconnsubb  23548  pthaus  23763  txhaus  23772  xkohaus  23778  regr1lem  23864  ustval  24328  methaus  24645  metnrmlem3  24987  pmltpclem1  25575  brslts  27920  bdayfinbndcbv  28624  bdayfinbndlem1  28625  bdayfinbndlem2  28626  axtgeucl  28706  iscgrad  29078  dfcgra2  29097  f1otrge  29161  axeuclidlem  29252  umgrvad2edg  29503  elwspths2spth  30259  upgr3v3e3cycl  30471  upgr4cycl4dv4e  30476  vdgn1frgrv2  30587  numclwlk1lem1  30660  ex-opab  30723  isnvlem  30902  ajval  31153  adjeu  32181  adjval  32182  adj1  32225  adjeq  32227  cnlnssadj  32372  br8d  32893  lt2addrd  33035  xlt2addrd  33044  crngmxidl  33696  constrconj  34079  constrllcllem  34086  constrcccllem  34088  constrcbvlem  34089  measval  34532  tz9.1regs  35469  loop1cycl  35527  br8  36146  br6  36147  br4  36148  brcgr3  36436  brsegle  36498  fvray  36531  linedegen  36533  fvline  36534  poimirlem28  38186  isopos  39843  hlsuprexch  40044  2llnjN  40230  2lplnj  40283  cdlemk42  41604  zindbi  43564  jm2.27  43626  nnoeomeqom  43930  tfsconcatrev  43966  rp-brsslt  44040  stoweidlem43  46648  fourierdlem42  46754  ichexmpl1  48106  vopnbgrel  48507  dfclnbgr6  48509  dfnbgr6  48510  cycl3grtri  48600  grimgrtri  48602  usgrgrtrirex  48603  grlimgrtri  48656  usgrexmpl1tri  48678  sepfsepc  49590  iscnrm3rlem8  49609  iscnrm3llem2  49612