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  2171  f1dom3el3dif  7277  xpord2lem  8166  xpord3lem  8173  frrlem1  8312  frrlem13  8324  cofsmo  10354  axdc3lem3  10537  axdc3lem4  10538  iscatd2  17864  psgnunilem1  19716  nn0gsumfz  20207  opprsubrg  20854  lsspropd  21301  mdetunilem3  22938  mdetunilem9  22944  smadiadetr  22999  lmres  23627  cnhaus  23681  regsep2  23703  dishaus  23709  ordthauslem  23710  nconnsubb  23750  pthaus  23966  txhaus  23975  xkohaus  23981  regr1lem  24067  ustval  24531  methaus  24848  metnrmlem3  25190  pmltpclem1  25778  brslts  28157  bdayfinbndcbv  28861  bdayfinbndlem1  28862  bdayfinbndlem2  28863  axtgeucl  28943  iscgrad  29327  dfcgra2  29347  f1otrge  29458  axeuclidlem  29549  umgrvad2edg  29803  elwspths2spth  30568  loop1cycl  30753  upgr3v3e3cycl  30790  upgr4cycl4dv4e  30795  vdgn1frgrv2  30906  numclwlk1lem1  30979  ex-opab  31042  isnvlem  31221  ajval  31472  adjeu  32500  adjval  32501  adj1  32544  adjeq  32546  cnlnssadj  32691  br8d  33253  lt2addrd  33392  xlt2addrd  33401  crngmxidl  34044  constrconj  34427  constrllcllem  34434  constrcccllem  34436  constrcbvlem  34437  measval  34881  tz9.1regs  35870  br8  36645  br6  36646  br4  36647  brcgr3  36935  brsegle  36997  fvray  37030  linedegen  37032  fvline  37033  poimirlem28  38703  isopos  40374  hlsuprexch  40575  2llnjN  40761  2lplnj  40814  cdlemk42  42135  zindbi  44090  jm2.27  44152  nnoeomeqom  44451  tfsconcatrev  44487  rp-brsslt  44561  stoweidlem43  47189  fourierdlem42  47295  ichexmpl1  48687  vopnbgrel  49088  dfclnbgr6  49090  dfnbgr6  49091  cycl3grtri  49181  grimgrtri  49183  usgrgrtrirex  49184  grlimgrtri  49237  usgrexmpl1tri  49259  sepfsepc  50178  iscnrm3rlem8  50197  iscnrm3llem2  50200