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  2138  f1dom3el3dif  7203  xpord2lem  8072  xpord3lem  8079  frrlem1  8216  frrlem13  8228  cofsmo  10160  axdc3lem3  10343  axdc3lem4  10344  iscatd2  17587  psgnunilem1  19405  nn0gsumfz  19896  opprsubrg  20508  lsspropd  20951  mdetunilem3  22529  mdetunilem9  22535  smadiadetr  22590  lmres  23215  cnhaus  23269  regsep2  23291  dishaus  23297  ordthauslem  23298  nconnsubb  23338  pthaus  23553  txhaus  23562  xkohaus  23568  regr1lem  23654  ustval  24118  methaus  24435  metnrmlem3  24777  pmltpclem1  25376  brsslt  27725  axtgeucl  28450  iscgrad  28789  dfcgra2  28808  f1otrge  28850  axeuclidlem  28940  umgrvad2edg  29191  elwspths2spth  29948  upgr3v3e3cycl  30160  upgr4cycl4dv4e  30165  vdgn1frgrv2  30276  numclwlk1lem1  30349  ex-opab  30412  isnvlem  30590  ajval  30841  adjeu  31869  adjval  31870  adj1  31913  adjeq  31915  cnlnssadj  32060  br8d  32591  lt2addrd  32734  xlt2addrd  32742  crngmxidl  33434  constrconj  33758  constrllcllem  33765  constrcccllem  33767  constrcbvlem  33768  measval  34211  tz9.1regs  35130  loop1cycl  35181  br8  35800  br6  35801  br4  35802  brcgr3  36090  brsegle  36152  fvray  36185  linedegen  36187  fvline  36188  poimirlem28  37687  isopos  39278  hlsuprexch  39479  2llnjN  39665  2lplnj  39718  cdlemk42  41039  zindbi  43038  jm2.27  43100  nnoeomeqom  43404  tfsconcatrev  43440  rp-brsslt  43515  stoweidlem43  46140  fourierdlem42  46246  ichexmpl1  47568  vopnbgrel  47953  dfclnbgr6  47955  dfnbgr6  47956  cycl3grtri  48046  grimgrtri  48048  usgrgrtrirex  48049  grlimgrtri  48102  usgrexmpl1tri  48124  sepfsepc  49027  iscnrm3rlem8  49046  iscnrm3llem2  49049