Theorem 3anbi13d 1437

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 1435	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  1441  ax12wdemo  2133  f1dom3el3dif  7289  xpord2lem  8166  xpord3lem  8173  frrlem1  8310  frrlem13  8322  wfrlem1OLD  8347  wfrlem3OLDa  8350  wfrlem15OLD  8362  cofsmo  10307  axdc3lem3  10490  axdc3lem4  10491  iscatd2  17726  psgnunilem1  19526  nn0gsumfz  20017  opprsubrg  20610  lsspropd  21034  mdetunilem3  22636  mdetunilem9  22642  smadiadetr  22697  lmres  23324  cnhaus  23378  regsep2  23400  dishaus  23406  ordthauslem  23407  nconnsubb  23447  pthaus  23662  txhaus  23671  xkohaus  23677  regr1lem  23763  ustval  24227  methaus  24549  metnrmlem3  24897  pmltpclem1  25497  brsslt  27845  axtgeucl  28495  iscgrad  28834  dfcgra2  28853  f1otrge  28895  axeuclidlem  28992  umgrvad2edg  29245  elwspths2spth  29997  upgr3v3e3cycl  30209  upgr4cycl4dv4e  30214  vdgn1frgrv2  30325  numclwlk1lem1  30398  ex-opab  30461  isnvlem  30639  ajval  30890  adjeu  31918  adjval  31919  adj1  31962  adjeq  31964  cnlnssadj  32109  br8d  32630  lt2addrd  32762  xlt2addrd  32769  crngmxidl  33477  constrconj  33750  measval  34179  loop1cycl  35122  br8  35736  br6  35737  br4  35738  brcgr3  36028  brsegle  36090  fvray  36123  linedegen  36125  fvline  36126  poimirlem28  37635  isopos  39162  hlsuprexch  39364  2llnjN  39550  2lplnj  39603  cdlemk42  40924  zindbi  42935  jm2.27  42997  nnoeomeqom  43302  tfsconcatrev  43338  rp-brsslt  43413  stoweidlem43  45999  fourierdlem42  46105  ichexmpl1  47394  vopnbgrel  47778  dfclnbgr6  47780  dfnbgr6  47781  grimgrtri  47852  usgrgrtrirex  47853  grlimgrtri  47899  usgrexmpl1tri  47920  sepfsepc  48724  iscnrm3rlem8  48744  iscnrm3llem2  48747