Theorem 3anbi13d 1392

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

Syntax hints:   → wi 4   ↔ wb 194   ∧ w3a 1030

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 195  df-an 384  df-3an 1032

This theorem is referenced by:  3anbi3d  1396  ax12wdemo  1998  f1dom3el3dif  6404  wfrlem1  7279  wfrlem3a  7282  wfrlem15  7294  cofsmo  8952  axdc3lem3  9135  axdc3lem4  9136  iscatd2  16114  psgnunilem1  17685  nn0gsumfz  18152  opprsubrg  18573  lsspropd  18787  mdetunilem3  20187  mdetunilem9  20193  smadiadetr  20248  lmres  20862  cnhaus  20916  regsep2  20938  dishaus  20944  ordthauslem  20945  nconsubb  20984  pthaus  21199  txhaus  21208  xkohaus  21214  regr1lem  21300  ustval  21764  methaus  22083  metnrmlem3  22420  pmltpclem1  22969  axtgeucl  25116  iscgrad  25449  dfcgra2  25467  f1otrge  25498  axeuclidlem  25588  2wlkonot  26186  2spthonot  26187  usg2spthonot0  26210  vdn0frgrav2  26344  vdgn0frgrav2  26345  vdn1frgrav2  26346  vdgn1frgrav2  26347  ex-opab  26475  isnvlem  26661  ajval  26935  adjeu  27966  adjval  27967  adj1  28010  adjeq  28012  cnlnssadj  28157  br8d  28636  lt2addrd  28737  xlt2addrd  28747  measval  29422  br8  30733  br6  30734  br4  30735  nofulllem5  30939  brcgr3  31157  brsegle  31219  fvray  31252  linedegen  31254  fvline  31255  poimirlem28  32431  isopos  33309  hlsuprexch  33509  2llnjN  33695  2lplnj  33748  cdlemk42  35071  zindbi  36353  jm2.27  36417  stoweidlem43  38760  fourierdlem42  38866  umgrvad2edg  40462  elwspths2spth  41193  upgr3v3e3cycl  41369  upgr4cycl4dv4e  41374  vdgn1frgrv2  41488