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  17622  psgnunilem1  19407  nn0gsumfz  19898  opprsubrg  20513  lsspropd  20956  mdetunilem3  22534  mdetunilem9  22540  smadiadetr  22595  lmres  23220  cnhaus  23274  regsep2  23296  dishaus  23302  ordthauslem  23303  nconnsubb  23343  pthaus  23558  txhaus  23567  xkohaus  23573  regr1lem  23659  ustval  24123  methaus  24441  metnrmlem3  24783  pmltpclem1  25382  brsslt  27731  axtgeucl  28452  iscgrad  28791  dfcgra2  28810  f1otrge  28852  axeuclidlem  28942  umgrvad2edg  29193  elwspths2spth  29947  upgr3v3e3cycl  30159  upgr4cycl4dv4e  30164  vdgn1frgrv2  30275  numclwlk1lem1  30348  ex-opab  30411  isnvlem  30589  ajval  30840  adjeu  31868  adjval  31869  adj1  31912  adjeq  31914  cnlnssadj  32059  br8d  32588  lt2addrd  32724  xlt2addrd  32732  crngmxidl  33433  constrconj  33728  constrllcllem  33735  constrcccllem  33737  constrcbvlem  33738  measval  34181  loop1cycl  35117  br8  35736  br6  35737  br4  35738  brcgr3  36027  brsegle  36089  fvray  36122  linedegen  36124  fvline  36125  poimirlem28  37635  isopos  39166  hlsuprexch  39368  2llnjN  39554  2lplnj  39607  cdlemk42  40928  zindbi  42928  jm2.27  42990  nnoeomeqom  43294  tfsconcatrev  43330  rp-brsslt  43405  stoweidlem43  46034  fourierdlem42  46140  ichexmpl1  47463  vopnbgrel  47847  dfclnbgr6  47849  dfnbgr6  47850  cycl3grtri  47939  grimgrtri  47941  usgrgrtrirex  47942  grlimgrtri  47988  usgrexmpl1tri  48009  sepfsepc  48909  iscnrm3rlem8  48928  iscnrm3llem2  48931