Theorem 3anbi13d 1466

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anbi3d  1470  ax12wdemo  2172  f1dom3el3dif  7273  xpord2lem  8159  xpord3lem  8166  frrlem1  8304  frrlem13  8316  cofsmo  10347  axdc3lem3  10530  axdc3lem4  10531  iscatd2  17855  psgnunilem1  19707  nn0gsumfz  20198  opprsubrg  20845  lsspropd  21292  mdetunilem3  22929  mdetunilem9  22935  smadiadetr  22990  lmres  23618  cnhaus  23672  regsep2  23694  dishaus  23700  ordthauslem  23701  nconnsubb  23741  pthaus  23957  txhaus  23966  xkohaus  23972  regr1lem  24058  ustval  24522  methaus  24839  metnrmlem3  25181  pmltpclem1  25769  brslts  28148  bdayfinbndcbv  28852  bdayfinbndlem1  28853  bdayfinbndlem2  28854  axtgeucl  28934  iscgrad  29318  dfcgra2  29338  f1otrge  29449  axeuclidlem  29540  umgrvad2edg  29794  elwspths2spth  30559  loop1cycl  30744  upgr3v3e3cycl  30781  upgr4cycl4dv4e  30786  vdgn1frgrv2  30897  numclwlk1lem1  30970  ex-opab  31033  isnvlem  31212  ajval  31463  adjeu  32491  adjval  32492  adj1  32535  adjeq  32537  cnlnssadj  32682  br8d  33202  lt2addrd  33342  xlt2addrd  33351  crngmxidl  33994  constrconj  34377  constrllcllem  34384  constrcccllem  34386  constrcbvlem  34387  measval  34831  tz9.1regs  35802  br8  36521  br6  36522  br4  36523  brcgr3  36811  brsegle  36873  fvray  36906  linedegen  36908  fvline  36909  poimirlem28  38566  isopos  40237  hlsuprexch  40438  2llnjN  40624  2lplnj  40677  cdlemk42  41998  zindbi  43952  jm2.27  44014  nnoeomeqom  44313  tfsconcatrev  44349  rp-brsslt  44423  stoweidlem43  47052  fourierdlem42  47158  ichexmpl1  48550  vopnbgrel  48951  dfclnbgr6  48953  dfnbgr6  48954  cycl3grtri  49044  grimgrtri  49046  usgrgrtrirex  49047  grlimgrtri  49100  usgrexmpl1tri  49122  sepfsepc  50035  iscnrm3rlem8  50054  iscnrm3llem2  50057