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  2136  f1dom3el3dif  7226  xpord2lem  8098  xpord3lem  8105  frrlem1  8242  frrlem13  8254  cofsmo  10198  axdc3lem3  10381  axdc3lem4  10382  iscatd2  17618  psgnunilem1  19399  nn0gsumfz  19890  opprsubrg  20478  lsspropd  20900  mdetunilem3  22477  mdetunilem9  22483  smadiadetr  22538  lmres  23163  cnhaus  23217  regsep2  23239  dishaus  23245  ordthauslem  23246  nconnsubb  23286  pthaus  23501  txhaus  23510  xkohaus  23516  regr1lem  23602  ustval  24066  methaus  24384  metnrmlem3  24726  pmltpclem1  25325  brsslt  27673  axtgeucl  28375  iscgrad  28714  dfcgra2  28733  f1otrge  28775  axeuclidlem  28865  umgrvad2edg  29116  elwspths2spth  29870  upgr3v3e3cycl  30082  upgr4cycl4dv4e  30087  vdgn1frgrv2  30198  numclwlk1lem1  30271  ex-opab  30334  isnvlem  30512  ajval  30763  adjeu  31791  adjval  31792  adj1  31835  adjeq  31837  cnlnssadj  31982  br8d  32511  lt2addrd  32647  xlt2addrd  32655  crngmxidl  33413  constrconj  33708  constrllcllem  33715  constrcccllem  33717  constrcbvlem  33718  measval  34161  loop1cycl  35097  br8  35716  br6  35717  br4  35718  brcgr3  36007  brsegle  36069  fvray  36102  linedegen  36104  fvline  36105  poimirlem28  37615  isopos  39146  hlsuprexch  39348  2llnjN  39534  2lplnj  39587  cdlemk42  40908  zindbi  42908  jm2.27  42970  nnoeomeqom  43274  tfsconcatrev  43310  rp-brsslt  43385  stoweidlem43  46014  fourierdlem42  46120  ichexmpl1  47443  vopnbgrel  47827  dfclnbgr6  47829  dfnbgr6  47830  cycl3grtri  47919  grimgrtri  47921  usgrgrtrirex  47922  grlimgrtri  47968  usgrexmpl1tri  47989  sepfsepc  48889  iscnrm3rlem8  48908  iscnrm3llem2  48911