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  2173  f1dom3el3dif  7272  xpord2lem  8144  xpord3lem  8151  frrlem1  8289  frrlem13  8301  cofsmo  10268  axdc3lem3  10451  axdc3lem4  10452  iscatd2  17759  psgnunilem1  19607  nn0gsumfz  20098  opprsubrg  20742  lsspropd  21188  mdetunilem3  22821  mdetunilem9  22827  smadiadetr  22882  lmres  23507  cnhaus  23561  regsep2  23583  dishaus  23589  ordthauslem  23590  nconnsubb  23630  pthaus  23846  txhaus  23855  xkohaus  23861  regr1lem  23947  ustval  24411  methaus  24728  metnrmlem3  25070  pmltpclem1  25658  brslts  28006  bdayfinbndcbv  28710  bdayfinbndlem1  28711  bdayfinbndlem2  28712  axtgeucl  28792  iscgrad  29173  dfcgra2  29192  f1otrge  29276  axeuclidlem  29367  umgrvad2edg  29621  elwspths2spth  30386  loop1cycl  30571  upgr3v3e3cycl  30602  upgr4cycl4dv4e  30607  vdgn1frgrv2  30718  numclwlk1lem1  30791  ex-opab  30854  isnvlem  31033  ajval  31284  adjeu  32312  adjval  32313  adj1  32356  adjeq  32358  cnlnssadj  32503  br8d  33024  lt2addrd  33165  xlt2addrd  33174  crngmxidl  33816  constrconj  34199  constrllcllem  34206  constrcccllem  34208  constrcbvlem  34209  measval  34653  tz9.1regs  35604  br8  36285  br6  36286  br4  36287  brcgr3  36575  brsegle  36637  fvray  36670  linedegen  36672  fvline  36673  poimirlem28  38356  isopos  40012  hlsuprexch  40213  2llnjN  40399  2lplnj  40452  cdlemk42  41773  zindbi  43731  jm2.27  43793  nnoeomeqom  44097  tfsconcatrev  44133  rp-brsslt  44207  stoweidlem43  46815  fourierdlem42  46921  ichexmpl1  48276  vopnbgrel  48677  dfclnbgr6  48679  dfnbgr6  48680  cycl3grtri  48770  grimgrtri  48772  usgrgrtrirex  48773  grlimgrtri  48826  usgrexmpl1tri  48848  sepfsepc  49763  iscnrm3rlem8  49782  iscnrm3llem2  49785