Theorem 3anbi13d 1441

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 252	. 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂))
3		3anbi12d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	1, 2, 3	3anbi123d 1439	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜂 ∧ 𝜃) ↔ (𝜒 ∧ 𝜂 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ w3a 1054

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  3anbi3d  1445  ax12wdemo  2052  f1dom3el3dif  6566  wfrlem1  7459  wfrlem3a  7462  wfrlem15  7474  cofsmo  9129  axdc3lem3  9312  axdc3lem4  9313  iscatd2  16389  psgnunilem1  17959  nn0gsumfz  18426  opprsubrg  18849  lsspropd  19065  mdetunilem3  20468  mdetunilem9  20474  smadiadetr  20529  lmres  21152  cnhaus  21206  regsep2  21228  dishaus  21234  ordthauslem  21235  nconnsubb  21274  pthaus  21489  txhaus  21498  xkohaus  21504  regr1lem  21590  ustval  22053  methaus  22372  metnrmlem3  22711  pmltpclem1  23263  axtgeucl  25416  iscgrad  25748  dfcgra2  25766  f1otrge  25797  axeuclidlem  25887  umgrvad2edg  26150  elwspths2spth  26934  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  vdgn1frgrv2  27276  ex-opab  27419  isnvlem  27593  ajval  27845  adjeu  28876  adjval  28877  adj1  28920  adjeq  28922  cnlnssadj  29067  br8d  29548  lt2addrd  29644  xlt2addrd  29651  measval  30389  br8  31772  br6  31773  br4  31774  frrlem1  31905  brsslt  32025  brcgr3  32278  brsegle  32340  fvray  32373  linedegen  32375  fvline  32376  poimirlem28  33567  isopos  34785  hlsuprexch  34985  2llnjN  35171  2lplnj  35224  cdlemk42  36546  zindbi  37828  jm2.27  37892  stoweidlem43  40578  fourierdlem42  40684