Theorem 3anbi13d 1439

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3anbi3d  1443  ax12wdemo  2132  f1dom3el3dif  7268  xpord2lem  8128  xpord3lem  8135  frrlem1  8271  frrlem13  8283  wfrlem1OLD  8308  wfrlem3OLDa  8311  wfrlem15OLD  8323  cofsmo  10264  axdc3lem3  10447  axdc3lem4  10448  iscatd2  17625  psgnunilem1  19361  nn0gsumfz  19852  opprsubrg  20340  lsspropd  20628  mdetunilem3  22116  mdetunilem9  22122  smadiadetr  22177  lmres  22804  cnhaus  22858  regsep2  22880  dishaus  22886  ordthauslem  22887  nconnsubb  22927  pthaus  23142  txhaus  23151  xkohaus  23157  regr1lem  23243  ustval  23707  methaus  24029  metnrmlem3  24377  pmltpclem1  24965  brsslt  27287  axtgeucl  27723  iscgrad  28062  dfcgra2  28081  f1otrge  28123  axeuclidlem  28220  umgrvad2edg  28470  elwspths2spth  29221  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  vdgn1frgrv2  29549  numclwlk1lem1  29622  ex-opab  29685  isnvlem  29863  ajval  30114  adjeu  31142  adjval  31143  adj1  31186  adjeq  31188  cnlnssadj  31333  br8d  31839  lt2addrd  31964  xlt2addrd  31971  crngmxidl  32585  measval  33196  loop1cycl  34128  br8  34726  br6  34727  br4  34728  brcgr3  35018  brsegle  35080  fvray  35113  linedegen  35115  fvline  35116  poimirlem28  36516  isopos  38050  hlsuprexch  38252  2llnjN  38438  2lplnj  38491  cdlemk42  39812  zindbi  41685  jm2.27  41747  nnoeomeqom  42062  tfsconcatrev  42098  rp-brsslt  42174  stoweidlem43  44759  fourierdlem42  44865  ichexmpl1  46137  sepfsepc  47560  iscnrm3rlem8  47580  iscnrm3llem2  47583