Theorem 3anbi123d 1307

Description: Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.)

Hypotheses

Ref	Expression
bi3d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bi3d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))
bi3d.3	⊢ (𝜑 → (𝜂 ↔ 𝜁))

Assertion

Ref	Expression
3anbi123d	⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))

Proof of Theorem 3anbi123d

Step	Hyp	Ref	Expression
1		bi3d.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bi3d.2	. . . 4 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
3	1, 2	anbi12d 470	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
4		bi3d.3	. . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁))
5	3, 4	anbi12d 470	. 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁)))
6		df-3an 975	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
7		df-3an 975	. 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁))
8	5, 6, 7	3bitr4g 222	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  3anbi12d  1308  3anbi13d  1309  3anbi23d  1310  limeq  4362  smoeq  6269  tfrlemi1  6311  tfr1onlemaccex  6327  tfrcllemaccex  6340  ereq1  6520  updjud  7059  ctssdclemr  7089  elinp  7436  sup3exmid  8873  iccshftr  9951  iccshftl  9953  iccdil  9955  icccntr  9957  fzaddel  10015  elfzomelpfzo  10187  seq3f1olemstep  10457  seq3f1olemp  10458  sumeq1  11318  summodclem2  11345  summodc  11346  zsumdc  11347  prodmodclem2  11540  prodmodc  11541  divalglemnn  11877  divalglemeunn  11880  divalglemeuneg  11882  dfgcd2  11969  pythagtriplem18  12235  pythagtriplem19  12236  ctiunct  12395  ssomct  12400  isstruct2im  12426  isstruct2r  12427  fiinopn  12796  lmfval  12986  upxp  13066  2irrexpqap  13690  dceqnconst  14091  dcapnconst  14092